Theorem srecauxapp ≪ | index | src | ≫ 

theorem srecauxapp (S: set) (a n: nat): $ a < n -> srecaux S n @ a = srec S a $;
StepHypRefExpression
1 eqidd 
x = n -> a = a
2 id 
x = n -> x = n
3 1, 2 lteqd 
x = n -> (a < x <-> a < n)
4 eqsidd 
x = n -> S == S
5 4, 2 srecauxeqd 
x = n -> srecaux S x = srecaux S n
6 5 nseqd 
x = n -> srecaux S x == srecaux S n
7 6, 1 appeqd 
x = n -> srecaux S x @ a = srecaux S n @ a
8 eqidd 
x = n -> srec S a = srec S a
9 7, 8 eqeqd 
x = n -> (srecaux S x @ a = srec S a <-> srecaux S n @ a = srec S a)
10 3, 9 imeqd 
x = n -> (a < x -> srecaux S x @ a = srec S a <-> a < n -> srecaux S n @ a = srec S a)
11 eqidd 
x = 0 -> a = a
12 id 
x = 0 -> x = 0
13 11, 12 lteqd 
x = 0 -> (a < x <-> a < 0)
14 eqsidd 
x = 0 -> S == S
15 14, 12 srecauxeqd 
x = 0 -> srecaux S x = srecaux S 0
16 15 nseqd 
x = 0 -> srecaux S x == srecaux S 0
17 16, 11 appeqd 
x = 0 -> srecaux S x @ a = srecaux S 0 @ a
18 eqidd 
x = 0 -> srec S a = srec S a
19 17, 18 eqeqd 
x = 0 -> (srecaux S x @ a = srec S a <-> srecaux S 0 @ a = srec S a)
20 13, 19 imeqd 
x = 0 -> (a < x -> srecaux S x @ a = srec S a <-> a < 0 -> srecaux S 0 @ a = srec S a)
21 eqidd 
x = y -> a = a
22 id 
x = y -> x = y
23 21, 22 lteqd 
x = y -> (a < x <-> a < y)
24 eqsidd 
x = y -> S == S
25 24, 22 srecauxeqd 
x = y -> srecaux S x = srecaux S y
26 25 nseqd 
x = y -> srecaux S x == srecaux S y
27 26, 21 appeqd 
x = y -> srecaux S x @ a = srecaux S y @ a
28 eqidd 
x = y -> srec S a = srec S a
29 27, 28 eqeqd 
x = y -> (srecaux S x @ a = srec S a <-> srecaux S y @ a = srec S a)
30 23, 29 imeqd 
x = y -> (a < x -> srecaux S x @ a = srec S a <-> a < y -> srecaux S y @ a = srec S a)
31 eqidd 
x = suc y -> a = a
32 id 
x = suc y -> x = suc y
33 31, 32 lteqd 
x = suc y -> (a < x <-> a < suc y)
34 eqsidd 
x = suc y -> S == S
35 34, 32 srecauxeqd 
x = suc y -> srecaux S x = srecaux S (suc y)
36 35 nseqd 
x = suc y -> srecaux S x == srecaux S (suc y)
37 36, 31 appeqd 
x = suc y -> srecaux S x @ a = srecaux S (suc y) @ a
38 eqidd 
x = suc y -> srec S a = srec S a
39 37, 38 eqeqd 
x = suc y -> (srecaux S x @ a = srec S a <-> srecaux S (suc y) @ a = srec S a)
40 33, 39 imeqd 
x = suc y -> (a < x -> srecaux S x @ a = srec S a <-> a < suc y -> srecaux S (suc y) @ a = srec S a)
41 absurd 
~a < 0 -> a < 0 -> srecaux S 0 @ a = srec S a
42 lt02 
~a < 0
43 41, 42 ax_mp 
a < 0 -> srecaux S 0 @ a = srec S a
44 leltsuc 
a <= y <-> a < suc y
45 leloe 
a <= y <-> a < y \/ a = y
46 appeq1 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y) -> srecaux S (suc y) @ a = write (srecaux S y) y (S @ srecaux S y) @ a
47 srecauxS 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y)
48 46, 47 ax_mp 
srecaux S (suc y) @ a = write (srecaux S y) y (S @ srecaux S y) @ a
49 writeNe 
a != y -> write (srecaux S y) y (S @ srecaux S y) @ a = srecaux S y @ a
50 ltne 
a < y -> a != y
51 49, 50 syl 
a < y -> write (srecaux S y) y (S @ srecaux S y) @ a = srecaux S y @ a
52 48, 51 syl5eq 
a < y -> srecaux S (suc y) @ a = srecaux S y @ a
53 52 eqeq1d 
a < y -> (srecaux S (suc y) @ a = srec S a <-> srecaux S y @ a = srec S a)
54 53 bi2d 
a < y -> srecaux S y @ a = srec S a -> srecaux S (suc y) @ a = srec S a
55 54 a2i 
(a < y -> srecaux S y @ a = srec S a) -> a < y -> srecaux S (suc y) @ a = srec S a
56 eqcom 
a = y -> y = a
57 56 suceqd 
a = y -> suc y = suc a
58 57 srecauxeq2d 
a = y -> srecaux S (suc y) = srecaux S (suc a)
59 58 appneq1d 
a = y -> srecaux S (suc y) @ a = srecaux S (suc a) @ a
60 59 conv srec 
a = y -> srecaux S (suc y) @ a = srec S a
61 60 a1i 
(a < y -> srecaux S y @ a = srec S a) -> a = y -> srecaux S (suc y) @ a = srec S a
62 55, 61 eord 
(a < y -> srecaux S y @ a = srec S a) -> a < y \/ a = y -> srecaux S (suc y) @ a = srec S a
63 45, 62 syl5bi 
(a < y -> srecaux S y @ a = srec S a) -> a <= y -> srecaux S (suc y) @ a = srec S a
64 44, 63 syl5bir 
(a < y -> srecaux S y @ a = srec S a) -> a < suc y -> srecaux S (suc y) @ a = srec S a
65 10, 20, 30, 40, 43, 64 ind 
a < n -> srecaux S n @ a = srec S a

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)