Theorem grecaux2Sx ≪ | index | src | ≫ 

theorem grecaux2Sx (F K: set) (k n x z: nat):
  $ n <= x -> grecaux2 z K F (suc x) n k = grecaux2 z K F x n (K @ (x, k)) $;
StepHypRefExpression
1 id 
a = n -> a = n
2 1 grecaux2eq5d 
a = n -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) n k
3 1 grecaux2eq5d 
a = n -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x n (K @ (x, k))
4 2, 3 eqeqd 
a = n -> (grecaux2 z K F (suc x) a k = grecaux2 z K F x a (K @ (x, k)) <-> grecaux2 z K F (suc x) n k = grecaux2 z K F x n (K @ (x, k)))
5 id 
a = 0 -> a = 0
6 5 grecaux2eq5d 
a = 0 -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) 0 k
7 5 grecaux2eq5d 
a = 0 -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x 0 (K @ (x, k))
8 6, 7 eqeqd 
a = 0 -> (grecaux2 z K F (suc x) a k = grecaux2 z K F x a (K @ (x, k)) <-> grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k)))
9 id 
a = b -> a = b
10 9 grecaux2eq5d 
a = b -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) b k
11 9 grecaux2eq5d 
a = b -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x b (K @ (x, k))
12 10, 11 eqeqd 
a = b -> (grecaux2 z K F (suc x) a k = grecaux2 z K F x a (K @ (x, k)) <-> grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)))
13 id 
a = suc b -> a = suc b
14 13 grecaux2eq5d 
a = suc b -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) (suc b) k
15 13 grecaux2eq5d 
a = suc b -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x (suc b) (K @ (x, k))
16 14, 15 eqeqd 
a = suc b -> (grecaux2 z K F (suc x) a k = grecaux2 z K F x a (K @ (x, k)) <-> grecaux2 z K F (suc x) (suc b) k = grecaux2 z K F x (suc b) (K @ (x, k)))
17 eqtr4 
grecaux2 z K F (suc x) 0 k = z -> grecaux2 z K F x 0 (K @ (x, k)) = z -> grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
18 grecaux20 
grecaux2 z K F (suc x) 0 k = z
19 17, 18 ax_mp 
grecaux2 z K F x 0 (K @ (x, k)) = z -> grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
20 grecaux20 
grecaux2 z K F x 0 (K @ (x, k)) = z
21 19, 20 ax_mp 
grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
22 21 a1i 
n <= x -> grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
23 grecaux2S 
grecaux2 z K F (suc x) (suc b) k = F @ (b, grecaux1 K (suc x) k (suc x - suc b), grecaux2 z K F (suc x) b k)
24 grecaux2S 
grecaux2 z K F x (suc b) (K @ (x, k)) = F @ (b, grecaux1 K x (K @ (x, k)) (x - suc b), grecaux2 z K F x b (K @ (x, k)))
25 grecaux1Sx 
grecaux1 K (suc x) k (suc (x - suc b)) = grecaux1 K x (K @ (x, k)) (x - suc b)
26 subSS 
suc x - suc b = x - b
27 eqsub1 
suc (x - suc b) + b = x -> x - b = suc (x - suc b)
28 addSass 
suc (x - suc b) + b = x - suc b + suc b
29 npcan 
suc b <= x -> x - suc b + suc b = x
30 letr 
suc b <= n -> n <= x -> suc b <= x
31 30 conv lt 
b < n -> n <= x -> suc b <= x
32 31 impcom 
n <= x /\ b < n -> suc b <= x
33 29, 32 syl 
n <= x /\ b < n -> x - suc b + suc b = x
34 28, 33 syl5eq 
n <= x /\ b < n -> suc (x - suc b) + b = x
35 27, 34 syl 
n <= x /\ b < n -> x - b = suc (x - suc b)
36 26, 35 syl5eq 
n <= x /\ b < n -> suc x - suc b = suc (x - suc b)
37 36 grecaux1eq4d 
n <= x /\ b < n -> grecaux1 K (suc x) k (suc x - suc b) = grecaux1 K (suc x) k (suc (x - suc b))
38 25, 37 syl6eq 
n <= x /\ b < n -> grecaux1 K (suc x) k (suc x - suc b) = grecaux1 K x (K @ (x, k)) (x - suc b)
39 38 anwl 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) -> grecaux1 K (suc x) k (suc x - suc b) = grecaux1 K x (K @ (x, k)) (x - suc b)
40 anr 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) -> grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k))
41 39, 40 preqd 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) ->
  grecaux1 K (suc x) k (suc x - suc b), grecaux2 z K F (suc x) b k = grecaux1 K x (K @ (x, k)) (x - suc b), grecaux2 z K F x b (K @ (x, k))
42 41 preq2d 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) ->
  b, grecaux1 K (suc x) k (suc x - suc b), grecaux2 z K F (suc x) b k = b, grecaux1 K x (K @ (x, k)) (x - suc b), grecaux2 z K F x b (K @ (x, k))
43 42 appeq2d 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) ->
  F @ (b, grecaux1 K (suc x) k (suc x - suc b), grecaux2 z K F (suc x) b k) = F @ (b, grecaux1 K x (K @ (x, k)) (x - suc b), grecaux2 z K F x b (K @ (x, k)))
44 23, 24, 43 eqtr4g 
n <= x /\ b < n /\ grecaux2 z K F (suc x) b k = grecaux2 z K F x b (K @ (x, k)) -> grecaux2 z K F (suc x) (suc b) k = grecaux2 z K F x (suc b) (K @ (x, k))
45 4, 8, 12, 16, 22, 44 indlt 
n <= x -> grecaux2 z K F (suc x) n k = grecaux2 z K F x n (K @ (x, k))

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)