Theorem lfnauxS ≪ | index | src | ≫ 

theorem lfnauxS (F: set) (k n: nat):
  $ lfnaux F k (suc n) = F @ k : lfnaux F (suc k) n $;
StepHypRefExpression
1 eqtr 
lfnaux F k (suc n) =
    (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) ->
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    F @ k : lfnaux F (suc k) n ->
  lfnaux F k (suc n) = F @ k : lfnaux F (suc k) n
2 grecS 
grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) (suc n) k =
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)))
3 2 conv lfnaux 
lfnaux F k (suc n) =
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)))
4 1, 3 ax_mp 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    F @ k : lfnaux F (suc k) n ->
  lfnaux F k (suc n) = F @ k : lfnaux F (suc k) n
5 eqtr 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n) ->
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n) = F @ k : lfnaux F (suc k) n ->
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    F @ k : lfnaux F (suc k) n
6 appeq2 
n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = n, k, lfnaux F (suc k) n ->
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n)
7 preq2 
k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = k, lfnaux F (suc k) n ->
  n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = n, k, lfnaux F (suc k) n
8 preq2 
grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = lfnaux F (suc k) n ->
  k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = k, lfnaux F (suc k) n
9 greceq5 
(\\ a1, \ a2, suc a2) @ (n, k) = suc k ->
  grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) =
    grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n (suc k)
10 9 conv lfnaux 
(\\ a1, \ a2, suc a2) @ (n, k) = suc k -> grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = lfnaux F (suc k) n
11 anr 
a1 = n /\ a2 = k -> a2 = k
12 11 suceqd 
a1 = n /\ a2 = k -> suc a2 = suc k
13 12 applamed 
a1 = n -> (\ a2, suc a2) @ k = suc k
14 13 appslame 
(\\ a1, \ a2, suc a2) @ (n, k) = suc k
15 10, 14 ax_mp 
grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = lfnaux F (suc k) n
16 8, 15 ax_mp 
k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = k, lfnaux F (suc k) n
17 7, 16 ax_mp 
n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k)) = n, k, lfnaux F (suc k) n
18 6, 17 ax_mp 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n)
19 5, 18 ax_mp 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n) = F @ k : lfnaux F (suc k) n ->
  (\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
    F @ k : lfnaux F (suc k) n
20 anlr 
a3 = n /\ a4 = k /\ a5 = lfnaux F (suc k) n -> a4 = k
21 20 appeq2d 
a3 = n /\ a4 = k /\ a5 = lfnaux F (suc k) n -> F @ a4 = F @ k
22 anr 
a3 = n /\ a4 = k /\ a5 = lfnaux F (suc k) n -> a5 = lfnaux F (suc k) n
23 21, 22 conseqd 
a3 = n /\ a4 = k /\ a5 = lfnaux F (suc k) n -> F @ a4 : a5 = F @ k : lfnaux F (suc k) n
24 23 applamed 
a3 = n /\ a4 = k -> (\ a5, F @ a4 : a5) @ lfnaux F (suc k) n = F @ k : lfnaux F (suc k) n
25 24 appslamed 
a3 = n -> (\\ a4, \ a5, F @ a4 : a5) @ (k, lfnaux F (suc k) n) = F @ k : lfnaux F (suc k) n
26 25 appslame 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, lfnaux F (suc k) n) = F @ k : lfnaux F (suc k) n
27 19, 26 ax_mp 
(\\ a3, \\ a4, \ a5, F @ a4 : a5) @ (n, k, grec 0 (\\ a1, \ a2, suc a2) (\\ a3, \\ a4, \ a5, F @ a4 : a5) n ((\\ a1, \ a2, suc a2) @ (n, k))) =
  F @ k : lfnaux F (suc k) n
28 4, 27 ax_mp 
lfnaux F k (suc n) = F @ k : lfnaux F (suc 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)