Theorem grecaux1Sx ≪ | index | src | ≫ 

theorem grecaux1Sx (K: set) (k n x: nat):
  $ grecaux1 K (suc x) k (suc n) = grecaux1 K x (K @ (x, k)) n $;
StepHypRefExpression
1 eqsidd 
a = n -> K == K
2 eqidd 
a = n -> suc x = suc x
3 eqidd 
a = n -> k = k
4 id 
a = n -> a = n
5 4 suceqd 
a = n -> suc a = suc n
6 1, 2, 3, 5 grecaux1eqd 
a = n -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc n)
7 eqidd 
a = n -> x = x
8 eqidd 
a = n -> K @ (x, k) = K @ (x, k)
9 1, 7, 8, 4 grecaux1eqd 
a = n -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) n
10 6, 9 eqeqd 
a = n -> (grecaux1 K (suc x) k (suc a) = grecaux1 K x (K @ (x, k)) a <-> grecaux1 K (suc x) k (suc n) = grecaux1 K x (K @ (x, k)) n)
11 eqsidd 
a = 0 -> K == K
12 eqidd 
a = 0 -> suc x = suc x
13 eqidd 
a = 0 -> k = k
14 id 
a = 0 -> a = 0
15 14 suceqd 
a = 0 -> suc a = suc 0
16 11, 12, 13, 15 grecaux1eqd 
a = 0 -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc 0)
17 eqidd 
a = 0 -> x = x
18 eqidd 
a = 0 -> K @ (x, k) = K @ (x, k)
19 11, 17, 18, 14 grecaux1eqd 
a = 0 -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) 0
20 16, 19 eqeqd 
a = 0 -> (grecaux1 K (suc x) k (suc a) = grecaux1 K x (K @ (x, k)) a <-> grecaux1 K (suc x) k (suc 0) = grecaux1 K x (K @ (x, k)) 0)
21 eqsidd 
a = b -> K == K
22 eqidd 
a = b -> suc x = suc x
23 eqidd 
a = b -> k = k
24 id 
a = b -> a = b
25 24 suceqd 
a = b -> suc a = suc b
26 21, 22, 23, 25 grecaux1eqd 
a = b -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc b)
27 eqidd 
a = b -> x = x
28 eqidd 
a = b -> K @ (x, k) = K @ (x, k)
29 21, 27, 28, 24 grecaux1eqd 
a = b -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) b
30 26, 29 eqeqd 
a = b -> (grecaux1 K (suc x) k (suc a) = grecaux1 K x (K @ (x, k)) a <-> grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b)
31 eqsidd 
a = suc b -> K == K
32 eqidd 
a = suc b -> suc x = suc x
33 eqidd 
a = suc b -> k = k
34 id 
a = suc b -> a = suc b
35 34 suceqd 
a = suc b -> suc a = suc (suc b)
36 31, 32, 33, 35 grecaux1eqd 
a = suc b -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc (suc b))
37 eqidd 
a = suc b -> x = x
38 eqidd 
a = suc b -> K @ (x, k) = K @ (x, k)
39 31, 37, 38, 34 grecaux1eqd 
a = suc b -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) (suc b)
40 36, 39 eqeqd 
a = suc b -> (grecaux1 K (suc x) k (suc a) = grecaux1 K x (K @ (x, k)) a <-> grecaux1 K (suc x) k (suc (suc b)) = grecaux1 K x (K @ (x, k)) (suc b))
41 eqtr 
grecaux1 K (suc x) k (suc 0) = K @ (suc x - suc 0, grecaux1 K (suc x) k 0) ->
  K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0 ->
  grecaux1 K (suc x) k (suc 0) = grecaux1 K x (K @ (x, k)) 0
42 grecaux1S 
grecaux1 K (suc x) k (suc 0) = K @ (suc x - suc 0, grecaux1 K (suc x) k 0)
43 41, 42 ax_mp 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0 -> grecaux1 K (suc x) k (suc 0) = grecaux1 K x (K @ (x, k)) 0
44 eqtr4 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = K @ (x, k) ->
  grecaux1 K x (K @ (x, k)) 0 = K @ (x, k) ->
  K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0
45 appeq2 
suc x - suc 0, grecaux1 K (suc x) k 0 = x, k -> K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = K @ (x, k)
46 preq 
suc x - suc 0 = x -> grecaux1 K (suc x) k 0 = k -> suc x - suc 0, grecaux1 K (suc x) k 0 = x, k
47 eqtr 
suc x - suc 0 = x - 0 -> x - 0 = x -> suc x - suc 0 = x
48 subSS 
suc x - suc 0 = x - 0
49 47, 48 ax_mp 
x - 0 = x -> suc x - suc 0 = x
50 sub02 
x - 0 = x
51 49, 50 ax_mp 
suc x - suc 0 = x
52 46, 51 ax_mp 
grecaux1 K (suc x) k 0 = k -> suc x - suc 0, grecaux1 K (suc x) k 0 = x, k
53 grecaux10 
grecaux1 K (suc x) k 0 = k
54 52, 53 ax_mp 
suc x - suc 0, grecaux1 K (suc x) k 0 = x, k
55 45, 54 ax_mp 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = K @ (x, k)
56 44, 55 ax_mp 
grecaux1 K x (K @ (x, k)) 0 = K @ (x, k) -> K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0
57 grecaux10 
grecaux1 K x (K @ (x, k)) 0 = K @ (x, k)
58 56, 57 ax_mp 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0
59 43, 58 ax_mp 
grecaux1 K (suc x) k (suc 0) = grecaux1 K x (K @ (x, k)) 0
60 grecaux1S 
grecaux1 K (suc x) k (suc (suc b)) = K @ (suc x - suc (suc b), grecaux1 K (suc x) k (suc b))
61 grecaux1S 
grecaux1 K x (K @ (x, k)) (suc b) = K @ (x - suc b, grecaux1 K x (K @ (x, k)) b)
62 subSS 
suc x - suc (suc b) = x - suc b
63 62 a1i 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b -> suc x - suc (suc b) = x - suc b
64 id 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b -> grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b
65 63, 64 preqd 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b -> suc x - suc (suc b), grecaux1 K (suc x) k (suc b) = x - suc b, grecaux1 K x (K @ (x, k)) b
66 65 appeq2d 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b ->
  K @ (suc x - suc (suc b), grecaux1 K (suc x) k (suc b)) = K @ (x - suc b, grecaux1 K x (K @ (x, k)) b)
67 60, 61, 66 eqtr4g 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b -> grecaux1 K (suc x) k (suc (suc b)) = grecaux1 K x (K @ (x, k)) (suc b)
68 10, 20, 30, 40, 59, 67 ind 
grecaux1 K (suc x) k (suc n) = grecaux1 K x (K @ (x, k)) n

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)