Theorem srecauxS ≪ | index | src | ≫

theorem srecauxS (S: set) (n: nat):
  $ srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n) $;


finite (write (srecaux S n) n (S @ srecaux S n)) ->
  (srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n) <-> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n)))
finite (srecaux S n) -> finite (write (srecaux S n) n (S @ srecaux S n))
finite (srecaux S n)
finite (write (srecaux S n) n (S @ srecaux S n))
srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n) <-> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
srecaux S (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) ->
  (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n)) ->
  srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
recn 0 (\\ a, \ b, lower (write b a (S @ b))) (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n)
srecaux S (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n)
(\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n)) ->
  srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
a = n /\ b = srecaux S n -> b = srecaux S n
a = n /\ b = srecaux S n -> b == srecaux S n
a = n /\ b = srecaux S n -> a = n
a = n /\ b = srecaux S n -> S @ b = S @ srecaux S n
a = n /\ b = srecaux S n -> write b a (S @ b) == write (srecaux S n) n (S @ srecaux S n)
a = n /\ b = srecaux S n -> lower (write b a (S @ b)) = lower (write (srecaux S n) n (S @ srecaux S n))
a = n -> (\ b, lower (write b a (S @ b))) @ srecaux S n = lower (write (srecaux S n) n (S @ srecaux S n))
(\\ a, \ b, lower (write b a (S @ b))) @ (n, srecaux S n) = lower (write (srecaux S n) n (S @ srecaux S n))
(\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n))
srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n)

Step	Hyp	Ref	Expression
1		eqlower2	finite (write (srecaux S n) n (S @ srecaux S n)) -> (srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n) <-> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n)))
2		writefin	finite (srecaux S n) -> finite (write (srecaux S n) n (S @ srecaux S n))
3		finns	finite (srecaux S n)
4	2, 3	ax_mp	finite (write (srecaux S n) n (S @ srecaux S n))
5	1, 4	ax_mp	srecaux S (suc n) == write (srecaux S n) n (S @ srecaux S n) <-> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
6		eqtr	srecaux S (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) -> (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n)) -> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
7		recnS	recn 0 (\\ a, \ b, lower (write b a (S @ b))) (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n)
8	7	conv srecaux	srecaux S (suc n) = (\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n)
9	6, 8	ax_mp	(\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n)) -> srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
10		anr	a = n /\ b = srecaux S n -> b = srecaux S n
11	10	nseqd	a = n /\ b = srecaux S n -> b == srecaux S n
12		anl	a = n /\ b = srecaux S n -> a = n
13	10	appeq2d	a = n /\ b = srecaux S n -> S @ b = S @ srecaux S n
14	11, 12, 13	writeeqd	a = n /\ b = srecaux S n -> write b a (S @ b) == write (srecaux S n) n (S @ srecaux S n)
15	14	lowereqd	a = n /\ b = srecaux S n -> lower (write b a (S @ b)) = lower (write (srecaux S n) n (S @ srecaux S n))
16	15	applamed	a = n -> (\ b, lower (write b a (S @ b))) @ srecaux S n = lower (write (srecaux S n) n (S @ srecaux S n))
17	16	appslame	(\\ a, \ b, lower (write b a (S @ b))) @ (n, srecaux S n) = lower (write (srecaux S n) n (S @ srecaux S n))
18	17	conv srecaux	(\\ a, \ b, lower (write b a (S @ b))) @ (n, recn 0 (\\ a, \ b, lower (write b a (S @ b))) n) = lower (write (srecaux S n) n (S @ srecaux S n))
19	9, 18	ax_mp	srecaux S (suc n) = lower (write (srecaux S n) n (S @ srecaux S n))
20	5, 19	mpbir	srecaux S (suc n) == write (srecaux S n) n (S @ srecaux 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)