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 eqidd 
a = n -> z = z
2 eqsidd 
a = n -> K == K
3 eqsidd 
a = n -> F == F
4 eqidd 
a = n -> suc x = suc x
5 id 
a = n -> a = n
6 eqidd 
a = n -> k = k
7 1, 2, 3, 4, 5, 6 grecaux2eqd 
a = n -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) n k
8 eqidd 
a = n -> x = x
9 eqidd 
a = n -> K @ (x, k) = K @ (x, k)
10 1, 2, 3, 8, 5, 9 grecaux2eqd 
a = n -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x n (K @ (x, k))
11 7, 10 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)))
12 eqidd 
a = 0 -> z = z
13 eqsidd 
a = 0 -> K == K
14 eqsidd 
a = 0 -> F == F
15 eqidd 
a = 0 -> suc x = suc x
16 id 
a = 0 -> a = 0
17 eqidd 
a = 0 -> k = k
18 12, 13, 14, 15, 16, 17 grecaux2eqd 
a = 0 -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) 0 k
19 eqidd 
a = 0 -> x = x
20 eqidd 
a = 0 -> K @ (x, k) = K @ (x, k)
21 12, 13, 14, 19, 16, 20 grecaux2eqd 
a = 0 -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x 0 (K @ (x, k))
22 18, 21 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)))
23 eqidd 
a = b -> z = z
24 eqsidd 
a = b -> K == K
25 eqsidd 
a = b -> F == F
26 eqidd 
a = b -> suc x = suc x
27 id 
a = b -> a = b
28 eqidd 
a = b -> k = k
29 23, 24, 25, 26, 27, 28 grecaux2eqd 
a = b -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) b k
30 eqidd 
a = b -> x = x
31 eqidd 
a = b -> K @ (x, k) = K @ (x, k)
32 23, 24, 25, 30, 27, 31 grecaux2eqd 
a = b -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x b (K @ (x, k))
33 29, 32 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)))
34 eqidd 
a = suc b -> z = z
35 eqsidd 
a = suc b -> K == K
36 eqsidd 
a = suc b -> F == F
37 eqidd 
a = suc b -> suc x = suc x
38 id 
a = suc b -> a = suc b
39 eqidd 
a = suc b -> k = k
40 34, 35, 36, 37, 38, 39 grecaux2eqd 
a = suc b -> grecaux2 z K F (suc x) a k = grecaux2 z K F (suc x) (suc b) k
41 eqidd 
a = suc b -> x = x
42 eqidd 
a = suc b -> K @ (x, k) = K @ (x, k)
43 34, 35, 36, 41, 38, 42 grecaux2eqd 
a = suc b -> grecaux2 z K F x a (K @ (x, k)) = grecaux2 z K F x (suc b) (K @ (x, k))
44 40, 43 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)))
45 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))
46 grecaux20 
grecaux2 z K F (suc x) 0 k = z
47 45, 46 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))
48 grecaux20 
grecaux2 z K F x 0 (K @ (x, k)) = z
49 47, 48 ax_mp 
grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
50 49 a1i 
n <= x -> grecaux2 z K F (suc x) 0 k = grecaux2 z K F x 0 (K @ (x, k))
51 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)
52 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)))
53 grecaux1Sx 
grecaux1 K (suc x) k (suc (x - suc b)) = grecaux1 K x (K @ (x, k)) (x - suc b)
54 subSS 
suc x - suc b = x - b
55 eqsub1 
suc (x - suc b) + b = x -> x - b = suc (x - suc b)
56 addSass 
suc (x - suc b) + b = x - suc b + suc b
57 npcan 
suc b <= x -> x - suc b + suc b = x
58 letr 
suc b <= n -> n <= x -> suc b <= x
59 58 conv lt 
b < n -> n <= x -> suc b <= x
60 59 impcom 
n <= x /\ b < n -> suc b <= x
61 57, 60 syl 
n <= x /\ b < n -> x - suc b + suc b = x
62 56, 61 syl5eq 
n <= x /\ b < n -> suc (x - suc b) + b = x
63 55, 62 syl 
n <= x /\ b < n -> x - b = suc (x - suc b)
64 54, 63 syl5eq 
n <= x /\ b < n -> suc x - suc b = suc (x - suc b)
65 64 grecaux1eq4d 
n <= x /\ b < n -> grecaux1 K (suc x) k (suc x - suc b) = grecaux1 K (suc x) k (suc (x - suc b))
66 53, 65 syl6eq 
n <= x /\ b < n -> grecaux1 K (suc x) k (suc x - suc b) = grecaux1 K x (K @ (x, k)) (x - suc b)
67 66 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)
68 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))
69 67, 68 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))
70 69 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))
71 70 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)))
72 51, 52, 71 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))
73 11, 22, 33, 44, 50, 72 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)