Theorem recS ≪ | index | src | ≫ 

pub theorem recS (z: nat) (S: set) (n: nat):
  $ rec z S (suc n) = S @ rec z S n $;
StepHypRefExpression
1
 
m = n -> suc m = suc n
2
 
m = n -> rec z S (suc m) = rec z S (suc n)
3
 
m = n -> rec z S m = rec z S n
4
 
m = n -> S @ rec z S m = S @ rec z S n
5
2, 4
 
m = n -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc n) = S @ rec z S n)
6
 
m = k -> suc m = suc k
7
 
m = k -> rec z S (suc m) = rec z S (suc k)
8
 
m = k -> rec z S m = rec z S k
9
 
m = k -> S @ rec z S m = S @ rec z S k
10
7, 9
 
m = k -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc k) = S @ rec z S k)
12
 
finite {x | x <= suc k}
13
 
E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
14
 
rec z S 0 = z
15
 
0 <= suc k
16
 
x = 0 -> (x <= suc k <-> 0 <= suc k)
17
 
x = 0 -> pset a @ x = pset a @ 0
18
 
~x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
20
 
x = suc k -> x != 0
21
conv ne
 
x = suc k -> ~x = 0
22
 
x = 0 -> ~x = suc k
23
 
x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
24
 
x = 0 -> rec z S x = rec z S 0
25
 
x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S 0
26
 
x = 0 -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ 0 = rec z S 0)
27
 
x = 0 -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> 0 <= suc k -> pset a @ 0 = rec z S 0)
28
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> 0 <= suc k -> pset a @ 0 = rec z S 0
29
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = rec z S 0
30
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z
31
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z
32
 
suc k <= suc k
33
 
x = suc k -> (x <= suc k <-> suc k <= suc k)
34
 
x = suc k -> pset a @ x = pset a @ suc k
35
 
x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = S @ rec z S k
36
 
x = suc k -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc k = S @ rec z S k)
37
 
x = suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc k <= suc k -> pset a @ suc k = S @ rec z S k)
38
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc k <= suc k -> pset a @ suc k = S @ rec z S k
39
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ suc k = S @ rec z S k
40
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  pset a @ suc k = S @ rec z S k
41
 
y <= k <-> y < suc k
42
 
y <= k <-> suc y <= suc k
43
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y <= k
44
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> suc y <= suc k
45
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
46
 
x = suc y -> (x <= suc k <-> suc y <= suc k)
47
 
x = suc y -> pset a @ x = pset a @ suc y
48
 
suc y = suc k <-> y = k
49
 
x = suc y -> (x = suc k <-> suc y = suc k)
50
 
x = suc y -> (x = suc k <-> y = k)
51
 
x = suc y -> S @ rec z S k = S @ rec z S k
52
 
x = suc y -> rec z S x = rec z S (suc y)
53
50, 51, 52
 
x = suc y -> if (x = suc k) (S @ rec z S k) (rec z S x) = if (y = k) (S @ rec z S k) (rec z S (suc y))
54
 
x = suc y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))
55
 
x = suc y ->
  (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))
56
 
A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
57
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  suc y <= suc k ->
  pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
58
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
59
 
y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k
60
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k
61
 
pset a @ y = rec z S y -> rec z S y = pset a @ y
62
 
x <= suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
63
 
x = y -> (x <= suc k <-> y <= suc k)
64
 
y <= k /\ x = y -> (x <= suc k <-> y <= suc k)
65
 
y <= k /\ x = y -> y <= k
66
 
k <= suc k
67
 
y <= k /\ x = y -> k <= suc k
68
 
y <= k /\ x = y -> y <= suc k
69
 
y <= k /\ x = y -> x <= suc k
70
 
y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
71
 
x = y -> pset a @ x = pset a @ y
72
 
y <= k /\ x = y -> pset a @ x = pset a @ y
73
 
x < suc k -> x != suc k
74
conv ne
 
x < suc k -> ~x = suc k
75
 
x <= k <-> x < suc k
76
 
x = y -> (x <= k <-> y <= k)
77
 
y <= k -> y <= k
78
 
y <= k -> x = y -> x <= k
79
 
y <= k /\ x = y -> x <= k
80
 
y <= k /\ x = y -> x < suc k
81
 
y <= k /\ x = y -> ~x = suc k
82
 
y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
83
 
x = y -> rec z S x = rec z S y
84
 
y <= k /\ x = y -> rec z S x = rec z S y
85
 
y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S y
86
 
y <= k /\ x = y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)
87
 
y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)
88
 
y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ y = rec z S y
89
 
y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y
90
 
y <= k -> A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y
91
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S y = pset a @ y
92
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  rec z S y = pset a @ y
93
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  rec z S y = pset a @ y
94
 
y = k -> rec z S y = rec z S k
95
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  rec z S y = rec z S k
96
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  pset a @ y = rec z S k
97
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  S @ (pset a @ y) = S @ rec z S k
98
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
99
 
~y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)
100
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)
101
 
y < k \/ y = k -> y = k \/ y < k
102
conv or
 
y < k \/ y = k -> ~y = k -> y < k
103
 
y <= k <-> y < k \/ y = k
104
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y < k \/ y = k
105
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> ~y = k -> y < k
106
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> y < k
107
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  A. m (m < k -> rec z S (suc m) = S @ rec z S m)
108
 
m = y -> (m < k <-> y < k)
109
 
m = y -> suc m = suc y
110
 
m = y -> rec z S (suc m) = rec z S (suc y)
111
 
m = y -> rec z S m = rec z S y
112
 
m = y -> S @ rec z S m = S @ rec z S y
113
 
m = y -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc y) = S @ rec z S y)
114
 
m = y -> (m < k -> rec z S (suc m) = S @ rec z S m <-> y < k -> rec z S (suc y) = S @ rec z S y)
115
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> y < k -> rec z S (suc y) = S @ rec z S y
116
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  y < k ->
  rec z S (suc y) = S @ rec z S y
117
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S (suc y) = S @ rec z S y
118
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S y = pset a @ y
119
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  S @ rec z S y = S @ (pset a @ y)
120
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S (suc y) = S @ (pset a @ y)
121
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
122
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
123
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  pset a @ suc y = S @ (pset a @ y)
124
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  y <= k ->
  pset a @ suc y = S @ (pset a @ y)
125
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  y < suc k ->
  pset a @ suc y = S @ (pset a @ y)
126
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  A. y (y < suc k -> pset a @ suc y = S @ (pset a @ y))
127
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S (suc k) = S @ rec z S k
128
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) ->
  E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S (suc k) = S @ rec z S k
129
 
A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k
130
 
T. /\ A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k
131
5, 10, 130
 
T. -> rec z S (suc n) = S @ rec z S n
132
 
rec z S (suc n) = S @ rec 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)