LEMMA 3

*******

ALL(x1):ALL(x2):[x1 e n & x2 e n

=> ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x1

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

& exp'(0,0)=x2

& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]]

This formal, machine-verified proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

AXIOMS USED

***********

1 Set(n)

Axiom

2 0 e n

Axiom

Induction Axiom

3 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [0 e a & ALL(b):[b e a => b+1 e a]

=> ALL(b):[b e n => b e a]]]

Axiom

4 1 e n

Axiom

5 ALL(a):ALL(b):[a e n & b e n => a+b e n]

Axiom

6 ALL(a):ALL(b):[a e n & b e n => a*b e n]

Axiom

7 ALL(a):[a e n => a*0=0]

Axiom

PROOF

*****

Suppose...

8 x1 e n & x2 e n

Premise

9 x1 e n

Split, 8

10 x2 e n

Split, 8

Suppose...

11 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x1

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

& exp'(0,0)=x2

& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

Premise

Define: exp

12 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

Split, 11

13 exp(0,0)=x1

Split, 11

14 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

Split, 11

15 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

Split, 11

Define: exp'

16 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

Split, 11

17 exp'(0,0)=x2

Split, 11

18 ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

Split, 11

19 ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

Split, 11

Prove: ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]

Suppose...

20 x e n & y e n

Premise

21 x e n

Split, 20

22 y e n

Split, 20

Prove: ~[x=0 & y=0] => exp(x,y)=exp'(x,y)

Suppose...

23 ~[x=0 & y=0]

Premise

24 ~~[x=0 => ~y=0]

Imply-And, 23

25 x=0 => ~y=0

Rem DNeg, 24

Two cases:

26 x=0 | ~x=0

Or Not

Case 1

Prove: x=0 => exp(x,y)=exp'(x,y)

Suppose...

27 x=0

Premise

28 ~y=0

Detach, 25, 27

Prove By Induction: ALL(a):[a e n => [~a=0 => exp(0,a)=0]]

Apply Subset Axiom

29 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~b=0 => exp(0,b)=0]]]

Subset, 1

30 Set(p) & ALL(b):[b e p <=> b e n & [~b=0 => exp(0,b)=0]]

E Spec, 29

Define: p

31 Set(p)

Split, 30

32 ALL(b):[b e p <=> b e n & [~b=0 => exp(0,b)=0]]

Split, 30

Apply Induction Axiom for set p

33 Set(p) & ALL(b):[b e p => b e n]

=> [0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]]

U Spec, 3

Prove: ALL(b):[b e p => b e n]

Suppose...

34 t e p

Premise

35 t e p <=> t e n & [~t=0 => exp(0,t)=0]

U Spec, 32

36 [t e p => t e n & [~t=0 => exp(0,t)=0]]

& [t e n & [~t=0 => exp(0,t)=0] => t e p]

Iff-And, 35

37 t e p => t e n & [~t=0 => exp(0,t)=0]

Split, 36

38 t e n & [~t=0 => exp(0,t)=0] => t e p

Split, 36

39 t e n & [~t=0 => exp(0,t)=0]

Detach, 37, 34

40 t e n

Split, 39

As Required:

41 ALL(b):[b e p => b e n]

4 Conclusion, 34

42 Set(p) & ALL(b):[b e p => b e n]

Join, 31, 41

Sufficient: For ALL(b):[b e n => b e p]

43 0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]

Detach, 33, 42

Prove: 0ep (Base Case)

44 0 e p <=> 0 e n & [~0=0 => exp(0,0)=0]

U Spec, 32

45 [0 e p => 0 e n & [~0=0 => exp(0,0)=0]]

& [0 e n & [~0=0 => exp(0,0)=0] => 0 e p]

Iff-And, 44

46 0 e p => 0 e n & [~0=0 => exp(0,0)=0]

Split, 45

47 0 e n & [~0=0 => exp(0,0)=0] => 0 e p

Split, 45

Prove: ~0=0 => exp(0,0)=0

Suppose...

48 ~0=0

Premise

49 0=0

Reflex

50 ~0=0 => exp(0,0)=0

Arb Cons, 49

51 exp(0,0)=0

Detach, 50, 48

As Required:

52 ~0=0 => exp(0,0)=0

4 Conclusion, 48

53 0 e n & [~0=0 => exp(0,0)=0]

Join, 2, 52

As Required:

54 0 e p

Detach, 47, 53

Prove: ALL(b):[b e p => b+1 e p] (Inductive Step)

Suppose...

55 t e p

Premise

56 t e p <=> t e n & [~t=0 => exp(0,t)=0]

U Spec, 32

57 [t e p => t e n & [~t=0 => exp(0,t)=0]]

& [t e n & [~t=0 => exp(0,t)=0] => t e p]

Iff-And, 56

58 t e p => t e n & [~t=0 => exp(0,t)=0]

Split, 57

59 t e n & [~t=0 => exp(0,t)=0] => t e p

Split, 57

60 t e n & [~t=0 => exp(0,t)=0]

Detach, 58, 55

61 t e n

Split, 60

62 ~t=0 => exp(0,t)=0

Split, 60

63 ~~t=0 | exp(0,t)=0

Imply-Or, 62

Two Sub-Cases:

64 t=0 | exp(0,t)=0

Rem DNeg, 63

65 t+1 e p <=> t+1 e n & [~t+1=0 => exp(0,t+1)=0]

U Spec, 32

66 [t+1 e p => t+1 e n & [~t+1=0 => exp(0,t+1)=0]]

& [t+1 e n & [~t+1=0 => exp(0,t+1)=0] => t+1 e p]

Iff-And, 65

67 t+1 e p => t+1 e n & [~t+1=0 => exp(0,t+1)=0]

Split, 66

68 t+1 e n & [~t+1=0 => exp(0,t+1)=0] => t+1 e p

Split, 66

69 t+1 e n & [~~t+1=0 | exp(0,t+1)=0] => t+1 e p

Imply-Or, 68

Sufficient:

70 t+1 e n & [t+1=0 | exp(0,t+1)=0] => t+1 e p

Rem DNeg, 69

Sub-Case 1

Prove: t=0 => t+1 e p

Suppose...

71 t=0

Premise

72 ALL(b):[t e n & b e n => t+b e n]

U Spec, 5

73 t e n & 1 e n => t+1 e n

U Spec, 72

74 t e n & 1 e n

Join, 61, 4

75 t+1 e n

Detach, 73, 74

76 ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]

U Spec, 15

77 0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0

U Spec, 76

78 0 e n & 0 e n

Join, 2, 2

79 exp(0,0+1)=exp(0,0)*0

Detach, 77, 78

80 exp(0,0+1)=x1*0

Substitute, 13, 79

81 x1 e n => x1*0=0

U Spec, 7

82 x1*0=0

Detach, 81, 9

83 exp(0,0+1)=0

Substitute, 82, 80

84 exp(0,t+1)=0

Substitute, 71, 83

85 t+1=0 | exp(0,t+1)=0

Arb Or, 84

86 t+1 e n & [t+1=0 | exp(0,t+1)=0]

Join, 75, 85

87 t+1 e p

Detach, 70, 86

Sub-Case 1

As Required:

88 t=0 => t+1 e p

4 Conclusion, 71

Sub-Case 2

Prove: exp(0,t)=0 => t+1 e p

Suppose...

89 exp(0,t)=0

Premise

90 ALL(b):[t e n & b e n => t+b e n]

U Spec, 5

91 t e n & 1 e n => t+1 e n

U Spec, 90

92 t e n & 1 e n

Join, 61, 4

93 t+1 e n

Detach, 91, 92

94 ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]

U Spec, 15

95 0 e n & t e n => exp(0,t+1)=exp(0,t)*0

U Spec, 94

96 0 e n & t e n

Join, 2, 61

97 exp(0,t+1)=exp(0,t)*0

Detach, 95, 96

98 exp(0,t+1)=0*0

Substitute, 89, 97

99 0 e n => 0*0=0

U Spec, 7

100 0*0=0

Detach, 99, 2

101 exp(0,t+1)=0

Substitute, 100, 98

102 t+1=0 | exp(0,t+1)=0

Arb Or, 101

103 t+1 e n & [t+1=0 | exp(0,t+1)=0]

Join, 93, 102

104 t+1 e p

Detach, 70, 103

Sub-Case 2

As Required:

105 exp(0,t)=0 => t+1 e p

4 Conclusion, 89

106 [t=0 => t+1 e p] & [exp(0,t)=0 => t+1 e p]

Join, 88, 105

107 t+1 e p

Cases, 64, 106

As Required:

108 ALL(b):[b e p => b+1 e p]

4 Conclusion, 55

109 0 e p & ALL(b):[b e p => b+1 e p]

Join, 54, 108

As Required:

110 ALL(b):[b e n => b e p]

Detach, 43, 109

Prove: ALL(a):[a e n => [~a=0 => exp(0,a)=0]]

Suppose...

111 t e n

Premise

112 t e n => t e p

U Spec, 110

113 t e p

Detach, 112, 111

114 t e p <=> t e n & [~t=0 => exp(0,t)=0]

U Spec, 32

115 [t e p => t e n & [~t=0 => exp(0,t)=0]]

& [t e n & [~t=0 => exp(0,t)=0] => t e p]

Iff-And, 114

116 t e p => t e n & [~t=0 => exp(0,t)=0]

Split, 115

117 t e n & [~t=0 => exp(0,t)=0] => t e p

Split, 115

118 t e n & [~t=0 => exp(0,t)=0]

Detach, 116, 113

119 t e n

Split, 118

120 ~t=0 => exp(0,t)=0

Split, 118

As Required:

121 ALL(a):[a e n => [~a=0 => exp(0,a)=0]]

4 Conclusion, 111

122 y e n => [~y=0 => exp(0,y)=0]

U Spec, 121

123 ~y=0 => exp(0,y)=0

Detach, 122, 22

124 exp(0,y)=0

Detach, 123, 28

125 exp(x,y)=0

Substitute, 27, 124

126 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~b=0 => exp'(0,b)=0]]]

Subset, 1

127 Set(p2) & ALL(b):[b e p2 <=> b e n & [~b=0 => exp'(0,b)=0]]

E Spec, 126

Define: p2

128 Set(p2)

Split, 127

129 ALL(b):[b e p2 <=> b e n & [~b=0 => exp'(0,b)=0]]

Split, 127

130 Set(p2) & ALL(b):[b e p2 => b e n]

=> [0 e p2 & ALL(b):[b e p2 => b+1 e p2]

=> ALL(b):[b e n => b e p2]]

U Spec, 3

Prove: ALL(b):[b e p2 => b e n]

Suppose...

131 t e p2

Premise

132 t e p2 <=> t e n & [~t=0 => exp'(0,t)=0]

U Spec, 129

133 [t e p2 => t e n & [~t=0 => exp'(0,t)=0]]

& [t e n & [~t=0 => exp'(0,t)=0] => t e p2]

Iff-And, 132

134 t e p2 => t e n & [~t=0 => exp'(0,t)=0]

Split, 133

135 t e n & [~t=0 => exp'(0,t)=0] => t e p2

Split, 133

136 t e n & [~t=0 => exp'(0,t)=0]

Detach, 134, 131

137 t e n

Split, 136

As Required:

138 ALL(b):[b e p2 => b e n]

4 Conclusion, 131

139 Set(p2) & ALL(b):[b e p2 => b e n]

Join, 128, 138

Sufficient:

140 0 e p2 & ALL(b):[b e p2 => b+1 e p2]

=> ALL(b):[b e n => b e p2]

Detach, 130, 139

141 0 e p2 <=> 0 e n & [~0=0 => exp'(0,0)=0]

U Spec, 129

142 [0 e p2 => 0 e n & [~0=0 => exp'(0,0)=0]]

& [0 e n & [~0=0 => exp'(0,0)=0] => 0 e p2]

Iff-And, 141

143 0 e p2 => 0 e n & [~0=0 => exp'(0,0)=0]

Split, 142

144 0 e n & [~0=0 => exp'(0,0)=0] => 0 e p2

Split, 142

Prove: ~0=0 => exp'(0,0)=0

Suppose...

145 ~0=0

Premise

146 0=0

Reflex

147 ~0=0 => exp'(0,0)=0

Arb Cons, 146

148 exp'(0,0)=0

Detach, 147, 145

As Required:

149 ~0=0 => exp'(0,0)=0

4 Conclusion, 145

150 0 e n & [~0=0 => exp'(0,0)=0]

Join, 2, 149

As Required:

151 0 e p2

Detach, 144, 150

Prove: ALL(t):[t e p2 => t+1 e p2]

Suppose...

152 t e p2

Premise

153 t e p2 <=> t e n & [~t=0 => exp'(0,t)=0]

U Spec, 129

154 [t e p2 => t e n & [~t=0 => exp'(0,t)=0]]

& [t e n & [~t=0 => exp'(0,t)=0] => t e p2]

Iff-And, 153

155 t e p2 => t e n & [~t=0 => exp'(0,t)=0]

Split, 154

156 t e n & [~t=0 => exp'(0,t)=0] => t e p2

Split, 154

157 t e n & [~t=0 => exp'(0,t)=0]

Detach, 155, 152

158 t e n

Split, 157

159 ~t=0 => exp'(0,t)=0

Split, 157

160 ~~t=0 | exp'(0,t)=0

Imply-Or, 159

Two Sub-Cases:

161 t=0 | exp'(0,t)=0

Rem DNeg, 160

162 t+1 e p2 <=> t+1 e n & [~t+1=0 => exp'(0,t+1)=0]

U Spec, 129

163 [t+1 e p2 => t+1 e n & [~t+1=0 => exp'(0,t+1)=0]]

& [t+1 e n & [~t+1=0 => exp'(0,t+1)=0] => t+1 e p2]

Iff-And, 162

164 t+1 e p2 => t+1 e n & [~t+1=0 => exp'(0,t+1)=0]

Split, 163

165 t+1 e n & [~t+1=0 => exp'(0,t+1)=0] => t+1 e p2

Split, 163

166 t+1 e n & [~~t+1=0 | exp'(0,t+1)=0] => t+1 e p2

Imply-Or, 165

Sufficient: t+1 e p2

167 t+1 e n & [t+1=0 | exp'(0,t+1)=0] => t+1 e p2

Rem DNeg, 166

Sub-Case 1

168 t=0

Premise

169 ALL(b):[t e n & b e n => t+b e n]

U Spec, 5

170 t e n & 1 e n => t+1 e n

U Spec, 169

171 t e n & 1 e n

Join, 158, 4

172 t+1 e n

Detach, 170, 171

173 ALL(b):[0 e n & b e n => exp'(0,b+1)=exp'(0,b)*0]

U Spec, 19

174 0 e n & 0 e n => exp'(0,0+1)=exp'(0,0)*0

U Spec, 173

175 0 e n & 0 e n

Join, 2, 2

176 exp'(0,0+1)=exp'(0,0)*0

Detach, 174, 175

177 exp'(0,0+1)=x2*0

Substitute, 17, 176

178 x2 e n => x2*0=0

U Spec, 7

179 x2*0=0

Detach, 178, 10

180 exp'(0,0+1)=0

Substitute, 179, 177

181 exp'(0,t+1)=0

Substitute, 168, 180

182 t+1=0 | exp'(0,t+1)=0

Arb Or, 181

183 t+1 e n & [t+1=0 | exp'(0,t+1)=0]

Join, 172, 182

184 t+1 e p2

Detach, 167, 183

Sub-Case 1

As Required:

185 t=0 => t+1 e p2

4 Conclusion, 168

Sub-Case 2

Suppose...

186 exp'(0,t)=0

Premise

187 ALL(b):[t e n & b e n => t+b e n]

U Spec, 5

188 t e n & 1 e n => t+1 e n

U Spec, 187

189 t e n & 1 e n

Join, 158, 4

190 t+1 e n

Detach, 188, 189

191 ALL(b):[0 e n & b e n => exp'(0,b+1)=exp'(0,b)*0]

U Spec, 19

192 0 e n & t e n => exp'(0,t+1)=exp'(0,t)*0

U Spec, 191

193 0 e n & t e n

Join, 2, 158

194 exp'(0,t+1)=exp'(0,t)*0

Detach, 192, 193

195 exp'(0,t+1)=0*0

Substitute, 186, 194

196 0 e n => 0*0=0

U Spec, 7

197 0*0=0

Detach, 196, 2

198 exp'(0,t+1)=0

Substitute, 197, 195

199 t+1=0 | exp'(0,t+1)=0

Arb Or, 198

200 t+1 e n & [t+1=0 | exp'(0,t+1)=0]

Join, 190, 199

201 t+1 e p2

Detach, 167, 200

Sub-Case 2

As Required:

202 exp'(0,t)=0 => t+1 e p2

4 Conclusion, 186

203 [t=0 => t+1 e p2] & [exp'(0,t)=0 => t+1 e p2]

Join, 185, 202

204 t+1 e p2

Cases, 161, 203

As Required:

205 ALL(t):[t e p2 => t+1 e p2]

4 Conclusion, 152

206 0 e p2 & ALL(t):[t e p2 => t+1 e p2]

Join, 151, 205

As Required:

207 ALL(b):[b e n => b e p2]

Detach, 140, 206

Prove: ALL(a):[a e n => [~a=0 => exp'(0,a)=0]]

Suppose...

208 t e n

Premise

209 t e n => t e p2

U Spec, 207

210 t e p2

Detach, 209, 208

211 t e p2 <=> t e n & [~t=0 => exp'(0,t)=0]

U Spec, 129

212 [t e p2 => t e n & [~t=0 => exp'(0,t)=0]]

& [t e n & [~t=0 => exp'(0,t)=0] => t e p2]

Iff-And, 211

213 t e p2 => t e n & [~t=0 => exp'(0,t)=0]

Split, 212

214 t e n & [~t=0 => exp'(0,t)=0] => t e p2

Split, 212

215 t e n & [~t=0 => exp'(0,t)=0]

Detach, 213, 210

216 t e n

Split, 215

217 ~t=0 => exp'(0,t)=0

Split, 215

As Required:

218 ALL(a):[a e n => [~a=0 => exp'(0,a)=0]]

4 Conclusion, 208

219 y e n => [~y=0 => exp'(0,y)=0]

U Spec, 218

220 ~y=0 => exp'(0,y)=0

Detach, 219, 22

221 exp'(0,y)=0

Detach, 220, 28

222 exp'(x,y)=0

Substitute, 27, 221

223 exp(x,y)=exp'(x,y)

Substitute, 222, 125

Case 1

As Required:

224 x=0 => exp(x,y)=exp'(x,y)

4 Conclusion, 27

Case 2

225 ~x=0

Premise

226 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & exp(x,b)=exp'(x,b)]]

Subset, 1

227 Set(p3) & ALL(b):[b e p3 <=> b e n & exp(x,b)=exp'(x,b)]

E Spec, 226

Define: p3

228 Set(p3)

Split, 227

229 ALL(b):[b e p3 <=> b e n & exp(x,b)=exp'(x,b)]

Split, 227

230 Set(p3) & ALL(b):[b e p3 => b e n]

=> [0 e p3 & ALL(b):[b e p3 => b+1 e p3]

=> ALL(b):[b e n => b e p3]]

U Spec, 3

Prove: ALL(b):[b e p3 => b e n]

Suppose...

231 t e p3

Premise

232 t e p3 <=> t e n & exp(x,t)=exp'(x,t)

U Spec, 229

233 [t e p3 => t e n & exp(x,t)=exp'(x,t)]

& [t e n & exp(x,t)=exp'(x,t) => t e p3]

Iff-And, 232

234 t e p3 => t e n & exp(x,t)=exp'(x,t)

Split, 233

235 t e n & exp(x,t)=exp'(x,t) => t e p3

Split, 233

236 t e n & exp(x,t)=exp'(x,t)

Detach, 234, 231

237 t e n

Split, 236

As Required:

238 ALL(b):[b e p3 => b e n]

4 Conclusion, 231

239 Set(p3) & ALL(b):[b e p3 => b e n]

Join, 228, 238

Sufficient:

240 0 e p3 & ALL(b):[b e p3 => b+1 e p3]

=> ALL(b):[b e n => b e p3]

Detach, 230, 239

241 0 e p3 <=> 0 e n & exp(x,0)=exp'(x,0)

U Spec, 229

242 [0 e p3 => 0 e n & exp(x,0)=exp'(x,0)]

& [0 e n & exp(x,0)=exp'(x,0) => 0 e p3]

Iff-And, 241

243 0 e p3 => 0 e n & exp(x,0)=exp'(x,0)

Split, 242

Sufficient:

244 0 e n & exp(x,0)=exp'(x,0) => 0 e p3

Split, 242

245 x e n => [~x=0 => exp(x,0)=1]

U Spec, 14

246 ~x=0 => exp(x,0)=1

Detach, 245, 21

247 exp(x,0)=1

Detach, 246, 225

248 x e n => [~x=0 => exp'(x,0)=1]

U Spec, 18

249 ~x=0 => exp'(x,0)=1

Detach, 248, 21

250 exp'(x,0)=1

Detach, 249, 225

251 exp(x,0)=exp'(x,0)

Substitute, 250, 247

252 0 e n & exp(x,0)=exp'(x,0)

Join, 2, 251

As Required:

253 0 e p3

Detach, 244, 252

Prove: ALL(b):[b e p3 => b+1 e p3]

Suppose...

254 t e p3

Premise

255 t e p3 <=> t e n & exp(x,t)=exp'(x,t)

U Spec, 229

256 [t e p3 => t e n & exp(x,t)=exp'(x,t)]

& [t e n & exp(x,t)=exp'(x,t) => t e p3]

Iff-And, 255

257 t e p3 => t e n & exp(x,t)=exp'(x,t)

Split, 256

258 t e n & exp(x,t)=exp'(x,t) => t e p3

Split, 256

259 t e n & exp(x,t)=exp'(x,t)

Detach, 257, 254

260 t e n

Split, 259

261 exp(x,t)=exp'(x,t)

Split, 259

262 t+1 e p3 <=> t+1 e n & exp(x,t+1)=exp'(x,t+1)

U Spec, 229

263 [t+1 e p3 => t+1 e n & exp(x,t+1)=exp'(x,t+1)]

& [t+1 e n & exp(x,t+1)=exp'(x,t+1) => t+1 e p3]

Iff-And, 262

264 t+1 e p3 => t+1 e n & exp(x,t+1)=exp'(x,t+1)

Split, 263

Sufficient:

265 t+1 e n & exp(x,t+1)=exp'(x,t+1) => t+1 e p3

Split, 263

266 ALL(b):[t e n & b e n => t+b e n]

U Spec, 5

267 t e n & 1 e n => t+1 e n

U Spec, 266

268 t e n & 1 e n

Join, 260, 4

269 t+1 e n

Detach, 267, 268

270 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]

U Spec, 15

271 x e n & t e n => exp(x,t+1)=exp(x,t)*x

U Spec, 270

272 x e n & t e n

Join, 21, 260

273 exp(x,t+1)=exp(x,t)*x

Detach, 271, 272

274 exp(x,t+1)=exp'(x,t)*x

Substitute, 261, 273

275 exp(x,t)*x=exp'(x,t)*x

Substitute, 273, 274

276 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]

U Spec, 15

277 x e n & t e n => exp(x,t+1)=exp(x,t)*x

U Spec, 276

278 x e n & t e n

Join, 21, 260

279 exp(x,t+1)=exp(x,t)*x

Detach, 277, 278

280 ALL(b):[x e n & b e n => exp'(x,b+1)=exp'(x,b)*x]

U Spec, 19

281 x e n & t e n => exp'(x,t+1)=exp'(x,t)*x

U Spec, 280

282 exp'(x,t+1)=exp'(x,t)*x

Detach, 281, 278

283 exp'(x,t+1)=exp(x,t)*x

Substitute, 261, 282

284 exp(x,t+1)=exp'(x,t+1)

Substitute, 283, 279

285 t+1 e n & exp(x,t+1)=exp'(x,t+1)

Join, 269, 284

286 t+1 e p3

Detach, 265, 285

As Required:

287 ALL(b):[b e p3 => b+1 e p3]

4 Conclusion, 254

288 0 e p3 & ALL(b):[b e p3 => b+1 e p3]

Join, 253, 287

289 ALL(b):[b e n => b e p3]

Detach, 240, 288

290 y e n => y e p3

U Spec, 289

291 y e p3

Detach, 290, 22

292 y e p3 <=> y e n & exp(x,y)=exp'(x,y)

U Spec, 229

293 [y e p3 => y e n & exp(x,y)=exp'(x,y)]

& [y e n & exp(x,y)=exp'(x,y) => y e p3]

Iff-And, 292

294 y e p3 => y e n & exp(x,y)=exp'(x,y)

Split, 293

295 y e n & exp(x,y)=exp'(x,y) => y e p3

Split, 293

296 y e n & exp(x,y)=exp'(x,y)

Detach, 294, 291

297 y e n

Split, 296

298 exp(x,y)=exp'(x,y)

Split, 296

Case 2

As Required:

299 ~x=0 => exp(x,y)=exp'(x,y)

4 Conclusion, 225

300 [x=0 => exp(x,y)=exp'(x,y)]

& [~x=0 => exp(x,y)=exp'(x,y)]

Join, 224, 299

301 exp(x,y)=exp'(x,y)

Cases, 26, 300

As Required:

302 ~[x=0 & y=0] => exp(x,y)=exp'(x,y)

4 Conclusion, 23

As Required:

303 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]

4 Conclusion, 20

As Required:

304 ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x1

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

& exp'(0,0)=x2

& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

4 Conclusion, 11

As Required:

305 ALL(x1):ALL(x2):[x1 e n & x2 e n

=> ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x1

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

& exp'(0,0)=x2

& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]]

4 Conclusion, 8