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 id 
a = n -> a = n
2 1 suceqd 
a = n -> suc a = suc n
3 2 grecaux1eq4d 
a = n -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc n)
4 1 grecaux1eq4d 
a = n -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) n
5 3, 4 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)
6 id 
a = 0 -> a = 0
7 6 suceqd 
a = 0 -> suc a = suc 0
8 7 grecaux1eq4d 
a = 0 -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc 0)
9 6 grecaux1eq4d 
a = 0 -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) 0
10 8, 9 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)
11 id 
a = b -> a = b
12 11 suceqd 
a = b -> suc a = suc b
13 12 grecaux1eq4d 
a = b -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc b)
14 11 grecaux1eq4d 
a = b -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) b
15 13, 14 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)
16 id 
a = suc b -> a = suc b
17 16 suceqd 
a = suc b -> suc a = suc (suc b)
18 17 grecaux1eq4d 
a = suc b -> grecaux1 K (suc x) k (suc a) = grecaux1 K (suc x) k (suc (suc b))
19 16 grecaux1eq4d 
a = suc b -> grecaux1 K x (K @ (x, k)) a = grecaux1 K x (K @ (x, k)) (suc b)
20 18, 19 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))
21 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
22 grecaux1S 
grecaux1 K (suc x) k (suc 0) = K @ (suc x - suc 0, grecaux1 K (suc x) k 0)
23 21, 22 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
24 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
25 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)
26 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
27 eqtr 
suc x - suc 0 = x - 0 -> x - 0 = x -> suc x - suc 0 = x
28 subSS 
suc x - suc 0 = x - 0
29 27, 28 ax_mp 
x - 0 = x -> suc x - suc 0 = x
30 sub02 
x - 0 = x
31 29, 30 ax_mp 
suc x - suc 0 = x
32 26, 31 ax_mp 
grecaux1 K (suc x) k 0 = k -> suc x - suc 0, grecaux1 K (suc x) k 0 = x, k
33 grecaux10 
grecaux1 K (suc x) k 0 = k
34 32, 33 ax_mp 
suc x - suc 0, grecaux1 K (suc x) k 0 = x, k
35 25, 34 ax_mp 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = K @ (x, k)
36 24, 35 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
37 grecaux10 
grecaux1 K x (K @ (x, k)) 0 = K @ (x, k)
38 36, 37 ax_mp 
K @ (suc x - suc 0, grecaux1 K (suc x) k 0) = grecaux1 K x (K @ (x, k)) 0
39 23, 38 ax_mp 
grecaux1 K (suc x) k (suc 0) = grecaux1 K x (K @ (x, k)) 0
40 grecaux1S 
grecaux1 K (suc x) k (suc (suc b)) = K @ (suc x - suc (suc b), grecaux1 K (suc x) k (suc b))
41 grecaux1S 
grecaux1 K x (K @ (x, k)) (suc b) = K @ (x - suc b, grecaux1 K x (K @ (x, k)) b)
42 subSS 
suc x - suc (suc b) = x - suc b
43 42 a1i 
grecaux1 K (suc x) k (suc b) = grecaux1 K x (K @ (x, k)) b -> suc x - suc (suc b) = x - suc b
44 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
45 43, 44 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
46 45 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)
47 40, 41, 46 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)
48 5, 10, 15, 20, 39, 47 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)