Theorem lrecval ≪ | index | src | ≫ 

theorem lrecval (S: set) (n z: nat):
  $ lrec z S n =
    if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1)))) $;
StepHypRefExpression
1 eqtr 
lrec z S n = (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @ (\. x e. upto n, lrec z S x) ->
  (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @ (\. x e. upto n, lrec z S x) =
    if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1)))) ->
  lrec z S n = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
2 srecval 
srec (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) n =
  (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @
    (\. x e. upto n, srec (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) x)
3 2 conv lrec 
lrec z S n = (\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @ (\. x e. upto n, lrec z S x)
4 1, 3 ax_mp 
(\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @ (\. x e. upto n, lrec z S x) =
    if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1)))) ->
  lrec z S n = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
5 anr 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> i = size (Dom f)
6 sreclem 
f = \. x e. upto n, lrec z S x -> size (Dom f) = n
7 6 anwl 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> size (Dom f) = n
8 5, 7 eqtrd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> i = n
9 8 eqeq1d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> (i = 0 <-> n = 0)
10 9 ifeq1d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) ->
  if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1))) = if (n = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))
11 ifeq3a 
(~n = 0 -> S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)) = S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1)))) ->
  if (n = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1))) = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
12 8 subeq1d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> i - 1 = n - 1
13 12 fsteqd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> fst (i - 1) = fst (n - 1)
14 13 anwl 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> fst (i - 1) = fst (n - 1)
15 12 sndeqd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) -> snd (i - 1) = snd (n - 1)
16 15 anwl 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> snd (i - 1) = snd (n - 1)
17 16 appeq2d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> f @ snd (i - 1) = f @ snd (n - 1)
18 lreceq3 
x = snd (n - 1) -> lrec z S x = lrec z S (snd (n - 1))
19 18 sbne 
N[snd (n - 1) / x] lrec z S x = lrec z S (snd (n - 1))
20 sreclem2 
f = \. x e. upto n, lrec z S x -> snd (n - 1) < n -> f @ snd (n - 1) = N[snd (n - 1) / x] lrec z S x
21 anll 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> f = \. x e. upto n, lrec z S x
22 ltconsid2 
snd (n - 1) < fst (n - 1) : snd (n - 1)
23 consfstsnd 
n != 0 -> fst (n - 1) : snd (n - 1) = n
24 23 conv ne 
~n = 0 -> fst (n - 1) : snd (n - 1) = n
25 24 anwr 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> fst (n - 1) : snd (n - 1) = n
26 25 lteq2d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> (snd (n - 1) < fst (n - 1) : snd (n - 1) <-> snd (n - 1) < n)
27 22, 26 mpbii 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> snd (n - 1) < n
28 20, 21, 27 sylc 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> f @ snd (n - 1) = N[snd (n - 1) / x] lrec z S x
29 19, 28 syl6eq 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> f @ snd (n - 1) = lrec z S (snd (n - 1))
30 17, 29 eqtrd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> f @ snd (i - 1) = lrec z S (snd (n - 1))
31 16, 30 preqd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> snd (i - 1), f @ snd (i - 1) = snd (n - 1), lrec z S (snd (n - 1))
32 14, 31 preqd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 -> fst (i - 1), snd (i - 1), f @ snd (i - 1) = fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))
33 32 appeq2d 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) /\ ~n = 0 ->
  S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)) = S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1)))
34 11, 33 syla 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) ->
  if (n = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1))) = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
35 10, 34 eqtrd 
f = \. x e. upto n, lrec z S x /\ i = size (Dom f) ->
  if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1))) = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
36 35 sbned 
f = \. x e. upto n, lrec z S x ->
  N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1))) = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
37 36 applame 
(\ f, N[size (Dom f) / i] if (i = 0) z (S @ (fst (i - 1), snd (i - 1), f @ snd (i - 1)))) @ (\. x e. upto n, lrec z S x) =
  if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))
38 4, 37 ax_mp 
lrec z S n = if (n = 0) z (S @ (fst (n - 1), snd (n - 1), lrec z S (snd (n - 1))))

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)