Theorem grecS ≪ | index | src | ≫ 

theorem grecS (F K: set) (k n z: nat):
  $ grec z K F (suc n) k = F @ (n, k, grec z K F n (K @ (n, k))) $;
StepHypRefExpression
1 eqtr 
grec z K F (suc n) k = F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k) ->
  F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k) = F @ (n, k, grec z K F n (K @ (n, k))) ->
  grec z K F (suc n) k = F @ (n, k, grec z K F n (K @ (n, k)))
2 grecaux2S 
grecaux2 z K F (suc n) (suc n) k = F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k)
3 2 conv grec 
grec z K F (suc n) k = F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k)
4 1, 3 ax_mp 
F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k) = F @ (n, k, grec z K F n (K @ (n, k))) ->
  grec z K F (suc n) k = F @ (n, k, grec z K F n (K @ (n, k)))
5 appeq2 
n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = n, k, grec z K F n (K @ (n, k)) ->
  F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k) = F @ (n, k, grec z K F n (K @ (n, k)))
6 preq2 
grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = k, grec z K F n (K @ (n, k)) ->
  n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = n, k, grec z K F n (K @ (n, k))
7 preq 
grecaux1 K (suc n) k (suc n - suc n) = k ->
  grecaux2 z K F (suc n) n k = grec z K F n (K @ (n, k)) ->
  grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = k, grec z K F n (K @ (n, k))
8 eqtr 
grecaux1 K (suc n) k (suc n - suc n) = grecaux1 K (suc n) k 0 -> grecaux1 K (suc n) k 0 = k -> grecaux1 K (suc n) k (suc n - suc n) = k
9 grecaux1eq4 
suc n - suc n = 0 -> grecaux1 K (suc n) k (suc n - suc n) = grecaux1 K (suc n) k 0
10 subid 
suc n - suc n = 0
11 9, 10 ax_mp 
grecaux1 K (suc n) k (suc n - suc n) = grecaux1 K (suc n) k 0
12 8, 11 ax_mp 
grecaux1 K (suc n) k 0 = k -> grecaux1 K (suc n) k (suc n - suc n) = k
13 grecaux10 
grecaux1 K (suc n) k 0 = k
14 12, 13 ax_mp 
grecaux1 K (suc n) k (suc n - suc n) = k
15 7, 14 ax_mp 
grecaux2 z K F (suc n) n k = grec z K F n (K @ (n, k)) -> grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = k, grec z K F n (K @ (n, k))
16 grecaux2Sx 
n <= n -> grecaux2 z K F (suc n) n k = grecaux2 z K F n n (K @ (n, k))
17 16 conv grec 
n <= n -> grecaux2 z K F (suc n) n k = grec z K F n (K @ (n, k))
18 leid 
n <= n
19 17, 18 ax_mp 
grecaux2 z K F (suc n) n k = grec z K F n (K @ (n, k))
20 15, 19 ax_mp 
grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = k, grec z K F n (K @ (n, k))
21 6, 20 ax_mp 
n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k = n, k, grec z K F n (K @ (n, k))
22 5, 21 ax_mp 
F @ (n, grecaux1 K (suc n) k (suc n - suc n), grecaux2 z K F (suc n) n k) = F @ (n, k, grec z K F n (K @ (n, k)))
23 4, 22 ax_mp 
grec z K F (suc n) k = F @ (n, k, grec z K F n (K @ (n, 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)