Theorem lrecS ≪ | index | src | ≫ 

pub theorem lrecS (z: nat) (S: set) (a b: nat):
  $ lrec z S (a : b) = S @ (a, b, lrec z S b) $;
StepHypRefExpression
1 eqtr 
lrec z S (a : b) = if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) ->
  if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (a, b, lrec z S b) ->
  lrec z S (a : b) = S @ (a, b, lrec z S b)
2 lrecval 
lrec z S (a : b) = if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))))
3 1, 2 ax_mp 
if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (a, b, lrec z S b) -> lrec z S (a : b) = S @ (a, b, lrec z S b)
4 eqtr 
if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))) ->
  S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))) = S @ (a, b, lrec z S b) ->
  if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (a, b, lrec z S b)
5 ifneg 
~a : b = 0 ->
  if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))
6 consne0 
a : b != 0
7 6 conv ne 
~a : b = 0
8 5, 7 ax_mp 
if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))
9 4, 8 ax_mp 
S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))) = S @ (a, b, lrec z S b) ->
  if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (a, b, lrec z S b)
10 appeq2 
fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)) = a, b, lrec z S b ->
  S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))) = S @ (a, b, lrec z S b)
11 preq 
fst (a : b - 1) = a ->
  snd (a : b - 1), lrec z S (snd (a : b - 1)) = b, lrec z S b ->
  fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)) = a, b, lrec z S b
12 consfst 
fst (a : b - 1) = a
13 11, 12 ax_mp 
snd (a : b - 1), lrec z S (snd (a : b - 1)) = b, lrec z S b -> fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)) = a, b, lrec z S b
14 preq 
snd (a : b - 1) = b -> lrec z S (snd (a : b - 1)) = lrec z S b -> snd (a : b - 1), lrec z S (snd (a : b - 1)) = b, lrec z S b
15 conssnd 
snd (a : b - 1) = b
16 14, 15 ax_mp 
lrec z S (snd (a : b - 1)) = lrec z S b -> snd (a : b - 1), lrec z S (snd (a : b - 1)) = b, lrec z S b
17 lreceq3 
snd (a : b - 1) = b -> lrec z S (snd (a : b - 1)) = lrec z S b
18 17, 15 ax_mp 
lrec z S (snd (a : b - 1)) = lrec z S b
19 16, 18 ax_mp 
snd (a : b - 1), lrec z S (snd (a : b - 1)) = b, lrec z S b
20 13, 19 ax_mp 
fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)) = a, b, lrec z S b
21 10, 20 ax_mp 
S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1))) = S @ (a, b, lrec z S b)
22 9, 21 ax_mp 
if (a : b = 0) z (S @ (fst (a : b - 1), snd (a : b - 1), lrec z S (snd (a : b - 1)))) = S @ (a, b, lrec z S b)
23 3, 22 ax_mp 
lrec z S (a : b) = S @ (a, b, lrec z S b)

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)