Theorem recnS ≪ | index | src | ≫

theorem recnS (S: set) (n z: nat): $ recn z S (suc n) = S @ (n, recn z S n) $;


recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n) ->
  snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n) ->
  recn z S (suc n) = S @ (n, recn z S n)
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n -> snd (recnaux z S (suc n)) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n -> recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n
recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n) -> recn z S (suc n) = S @ (n, recn z S n)
snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ recnaux z S n ->
  S @ recnaux z S n = S @ (n, recn z S n) ->
  snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ recnaux z S n
S @ recnaux z S n = S @ (n, recn z S n) -> snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
recnaux z S n = n, recn z S n -> S @ recnaux z S n = S @ (n, recn z S n)
fst (recnaux z S n), snd (recnaux z S n) = recnaux z S n -> fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n -> recnaux z S n = n, recn z S n
fst (recnaux z S n), snd (recnaux z S n) = recnaux z S n
fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n -> recnaux z S n = n, recn z S n
fst (recnaux z S n) = n -> fst (recnaux z S n), snd (recnaux z S n) = n, snd (recnaux z S n)
fst (recnaux z S n) = n -> fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n
fst (recnaux z S n) = n
fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n
recnaux z S n = n, recn z S n
S @ recnaux z S n = S @ (n, recn z S n)
snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
recn z S (suc n) = S @ (n, recn z S n)

Step	Hyp	Ref	Expression
1		eqtr	recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n) -> snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n) -> recn z S (suc n) = S @ (n, recn z S n)
2		sndeq	recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n -> snd (recnaux z S (suc n)) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
3	2	conv recn	recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n -> recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
4		recnauxS2	recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n
5	3, 4	ax_mp	recn z S (suc n) = snd (suc (fst (recnaux z S n)), S @ recnaux z S n)
6	1, 5	ax_mp	snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n) -> recn z S (suc n) = S @ (n, recn z S n)
7		eqtr	snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ recnaux z S n -> S @ recnaux z S n = S @ (n, recn z S n) -> snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
8		sndpr	snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ recnaux z S n
9	7, 8	ax_mp	S @ recnaux z S n = S @ (n, recn z S n) -> snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
10		appeq2	recnaux z S n = n, recn z S n -> S @ recnaux z S n = S @ (n, recn z S n)
11		eqtr3	fst (recnaux z S n), snd (recnaux z S n) = recnaux z S n -> fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n -> recnaux z S n = n, recn z S n
12		fstsnd	fst (recnaux z S n), snd (recnaux z S n) = recnaux z S n
13	11, 12	ax_mp	fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n -> recnaux z S n = n, recn z S n
14		preq1	fst (recnaux z S n) = n -> fst (recnaux z S n), snd (recnaux z S n) = n, snd (recnaux z S n)
15	14	conv recn	fst (recnaux z S n) = n -> fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n
16		recnauxfst	fst (recnaux z S n) = n
17	15, 16	ax_mp	fst (recnaux z S n), snd (recnaux z S n) = n, recn z S n
18	13, 17	ax_mp	recnaux z S n = n, recn z S n
19	10, 18	ax_mp	S @ recnaux z S n = S @ (n, recn z S n)
20	9, 19	ax_mp	snd (suc (fst (recnaux z S n)), S @ recnaux z S n) = S @ (n, recn z S n)
21	6, 20	ax_mp	recn z S (suc n) = S @ (n, recn z S 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)