Step | Hyp | Ref | Expression |
1 |
|
eqtr |
grecaux2 z K F x (suc n) k = (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n)
->
(\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n) =
F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) ->
grecaux2 z K F x (suc n) k = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
2 |
|
recnS |
recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) (suc n) =
(\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n) |
3 |
2 |
conv grecaux2 |
grecaux2 z K F x (suc n) k = (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n) |
4 |
1, 3 |
ax_mp |
(\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n) =
F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) ->
grecaux2 z K F x (suc n) k = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
5 |
|
anl |
a1 = n /\ a2 = grecaux2 z K F x n k -> a1 = n |
6 |
5 |
suceqd |
a1 = n /\ a2 = grecaux2 z K F x n k -> suc a1 = suc n |
7 |
6 |
subeq2d |
a1 = n /\ a2 = grecaux2 z K F x n k -> x - suc a1 = x - suc n |
8 |
7 |
grecaux1eq4d |
a1 = n /\ a2 = grecaux2 z K F x n k -> grecaux1 K x k (x - suc a1) = grecaux1 K x k (x - suc n) |
9 |
|
anr |
a1 = n /\ a2 = grecaux2 z K F x n k -> a2 = grecaux2 z K F x n k |
10 |
8, 9 |
preqd |
a1 = n /\ a2 = grecaux2 z K F x n k -> grecaux1 K x k (x - suc a1), a2 = grecaux1 K x k (x - suc n), grecaux2 z K F x n k |
11 |
5, 10 |
preqd |
a1 = n /\ a2 = grecaux2 z K F x n k -> a1, grecaux1 K x k (x - suc a1), a2 = n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k |
12 |
11 |
appeq2d |
a1 = n /\ a2 = grecaux2 z K F x n k -> F @ (a1, grecaux1 K x k (x - suc a1), a2) = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
13 |
12 |
applamed |
a1 = n -> (\ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ grecaux2 z K F x n k = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
14 |
13 |
appslame |
(\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, grecaux2 z K F x n k) = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
15 |
14 |
conv grecaux2 |
(\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) @ (n, recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) n) =
F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |
16 |
4, 15 |
ax_mp |
grecaux2 z K F x (suc n) k = F @ (n, grecaux1 K x k (x - suc n), grecaux2 z K F x n k) |