THEOREM 2
*********
All "exponent-like" functions on the natural numbers are identical except for the values assigned to (0,0)
By Dan Christensen
October 2013
(This proof was written with the aid of the author's DC Proof software available at http://www.dcproof.com )
BASIC PRINCIPLES OF ARITHMETIC USED
***********************************
n is a set (the set of natural numbers)
1 Set(n)
Axiom
+ is a binary function on n
2 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
3 0 e n
Axiom
4 1 e n
Axiom
5 ALL(a):[a e n => a*0=0]
Axiom
The principle of mathematical induction (PMI)
6 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
Existence of predecessors
7 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & b+1=a]]]
Axiom
Suppose that pow and pow' are exponent-like functions such that pow(0,0)=x0 and pow'(0,0)=x1
8 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
& pow'(0,0)=x1
& ALL(a):[a e n => [~a=0 => pow'(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
Premise
Splitting this premise...
Define: pow
***********
9 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
Split, 8
10 pow(0,0)=x0
Split, 8
11 ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
Split, 8
12 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
Split, 8
Define: pow'
************
13 ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
Split, 8
14 pow'(0,0)=x1
Split, 8
15 ALL(a):[a e n => [~a=0 => pow'(a,0)=1]]
Split, 8
16 ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
Split, 8
Prove: ALL(a):[a e n => [~a=0 => pow(a,0)=pow'(a,0)]]
Suppose...
17 x e n
Premise
Prove: ~x=0 => pow(x,0)=pow'(x,0)
Suppose...
18 ~x=0
Premise
Apply definition of pow
19 x e n => [~x=0 => pow(x,0)=1]
U Spec, 11
20 ~x=0 => pow(x,0)=1
Detach, 19, 17
21 pow(x,0)=1
Detach, 20, 18
Apply definition of pow'
22 x e n => [~x=0 => pow'(x,0)=1]
U Spec, 15
23 ~x=0 => pow'(x,0)=1
Detach, 22, 17
24 pow'(x,0)=1
Detach, 23, 18
25 pow(x,0)=pow'(x,0)
Substitute, 24, 21
As Required:
26 ~x=0 => pow(x,0)=pow'(x,0)
4 Conclusion, 18
As Required:
27 ALL(a):[a e n => [~a=0 => pow(a,0)=pow'(a,0)]]
4 Conclusion, 17
Suppose...
28 x e n
Premise
Apply Subset Axiom for proof by induction
29 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & pow(x,b+1)=pow'(x,b+1)]]
Subset, 1
30 Set(p) & ALL(b):[b e p <=> b e n & pow(x,b+1)=pow'(x,b+1)]
E Spec, 29
Define: p
*********
31 Set(p)
Split, 30
32 ALL(b):[b e p <=> b e n & pow(x,b+1)=pow'(x,b+1)]
Split, 30
Apply PMI
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, 6
Prove: ALL(b):[b e p => b e n]
Suppose...
34 t e p
Premise
Apply definition of p
35 t e p <=> t e n & pow(x,t+1)=pow'(x,t+1)
U Spec, 32
36 [t e p => t e n & pow(x,t+1)=pow'(x,t+1)]
& [t e n & pow(x,t+1)=pow'(x,t+1) => t e p]
Iff-And, 35
37 t e p => t e n & pow(x,t+1)=pow'(x,t+1)
Split, 36
38 t e n & pow(x,t+1)=pow'(x,t+1) => t e p
Split, 36
39 t e n & pow(x,t+1)=pow'(x,t+1)
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: 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
Apply definition of p
44 0 e p <=> 0 e n & pow(x,0+1)=pow'(x,0+1)
U Spec, 32
45 [0 e p => 0 e n & pow(x,0+1)=pow'(x,0+1)]
& [0 e n & pow(x,0+1)=pow'(x,0+1) => 0 e p]
Iff-And, 44
46 0 e p => 0 e n & pow(x,0+1)=pow'(x,0+1)
Split, 45
Sufficient: 0 e p
47 0 e n & pow(x,0+1)=pow'(x,0+1) => 0 e p
Split, 45
Apply definition of pow
48 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
49 x e n & 0 e n => pow(x,0+1)=pow(x,0)*x
U Spec, 48
50 x e n & 0 e n
Join, 28, 3
51 pow(x,0+1)=pow(x,0)*x
Detach, 49, 50
Apply definition of pow'
52 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 16
53 x e n & 0 e n => pow'(x,0+1)=pow'(x,0)*x
U Spec, 52
54 pow'(x,0+1)=pow'(x,0)*x
Detach, 53, 50
Two cases:
55 x=0 | ~x=0
Or Not
Prove: x=0 => 0 e p
Suppose...
56 x=0
Premise
57 pow(x,0+1)=pow(x,0)*0
Substitute, 56, 51
58 pow(x,0) e n => pow(x,0)*0=0
U Spec, 5
Apply definition of pow
59 ALL(b):[x e n & b e n => pow(x,b) e n]
U Spec, 9
60 x e n & 0 e n => pow(x,0) e n
U Spec, 59
61 x e n & 0 e n
Join, 28, 3
62 pow(x,0) e n
Detach, 60, 61
63 pow(x,0)*0=0
Detach, 58, 62
64 pow(x,0+1)=0
Substitute, 63, 57
65 pow'(x,0+1)=pow'(x,0)*0
Substitute, 56, 54
66 pow'(x,0) e n => pow'(x,0)*0=0
U Spec, 5
Apply definition of pow'
67 ALL(b):[x e n & b e n => pow'(x,b) e n]
U Spec, 13
68 x e n & 0 e n => pow'(x,0) e n
U Spec, 67
69 pow'(x,0) e n
Detach, 68, 61
70 pow'(x,0)*0=0
Detach, 66, 69
71 pow'(x,0+1)=0
Substitute, 70, 65
72 pow(x,0+1)=pow'(x,0+1)
Substitute, 71, 64
73 0 e n & pow(x,0+1)=pow'(x,0+1)
Join, 3, 72
74 0 e p
Detach, 47, 73
As Required:
75 x=0 => 0 e p
4 Conclusion, 56
Prove: ~x=0 => 0 e p
76 ~x=0
Premise
Apply definition of pow
77 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
78 x e n & 0 e n => pow(x,0+1)=pow(x,0)*x
U Spec, 77
79 x e n & 0 e n
Join, 28, 3
80 pow(x,0+1)=pow(x,0)*x
Detach, 78, 79
Apply definition of pow'
81 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 16
82 x e n & 0 e n => pow'(x,0+1)=pow'(x,0)*x
U Spec, 81
83 pow'(x,0+1)=pow'(x,0)*x
Detach, 82, 79
84 x e n => [~x=0 => pow(x,0)=pow'(x,0)]
U Spec, 27
85 ~x=0 => pow(x,0)=pow'(x,0)
Detach, 84, 28
86 pow(x,0)=pow'(x,0)
Detach, 85, 76
87 pow'(x,0+1)=pow(x,0)*x
Substitute, 86, 83
88 pow(x,0+1)=pow'(x,0+1)
Substitute, 87, 80
89 0 e n & pow(x,0+1)=pow'(x,0+1)
Join, 3, 88
90 0 e p
Detach, 47, 89
As Required:
91 ~x=0 => 0 e p
4 Conclusion, 76
92 [x=0 => 0 e p] & [~x=0 => 0 e p]
Join, 75, 91
As Required:
93 0 e p
Cases, 55, 92
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
94 t e p
Premise
Apply definition of p
95 t e p <=> t e n & pow(x,t+1)=pow'(x,t+1)
U Spec, 32
96 [t e p => t e n & pow(x,t+1)=pow'(x,t+1)]
& [t e n & pow(x,t+1)=pow'(x,t+1) => t e p]
Iff-And, 95
97 t e p => t e n & pow(x,t+1)=pow'(x,t+1)
Split, 96
98 t e n & pow(x,t+1)=pow'(x,t+1) => t e p
Split, 96
99 t e n & pow(x,t+1)=pow'(x,t+1)
Detach, 97, 94
100 t e n
Split, 99
101 pow(x,t+1)=pow'(x,t+1)
Split, 99
Apply definition of p
102 t+1 e p <=> t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1)
U Spec, 32
103 [t+1 e p => t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1)]
& [t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1) => t+1 e p]
Iff-And, 102
104 t+1 e p => t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1)
Split, 103
Sufficient: t+1 e p
105 t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1) => t+1 e p
Split, 103
106 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
107 t e n & 1 e n => t+1 e n
U Spec, 106
108 t e n & 1 e n
Join, 100, 4
109 t+1 e n
Detach, 107, 108
Apply definition of pow
110 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
111 x e n & t+1 e n => pow(x,t+1+1)=pow(x,t+1)*x
U Spec, 110
112 x e n & t+1 e n
Join, 28, 109
113 pow(x,t+1+1)=pow(x,t+1)*x
Detach, 111, 112
Apply definition of pow'
114 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 16
115 x e n & t+1 e n => pow'(x,t+1+1)=pow'(x,t+1)*x
U Spec, 114
116 pow'(x,t+1+1)=pow'(x,t+1)*x
Detach, 115, 112
117 pow'(x,t+1+1)=pow(x,t+1)*x
Substitute, 101, 116
118 pow(x,t+1+1)=pow'(x,t+1+1)
Substitute, 117, 113
119 t+1 e n & pow(x,t+1+1)=pow'(x,t+1+1)
Join, 109, 118
120 t+1 e p
Detach, 105, 119
As Required:
121 ALL(b):[b e p => b+1 e p]
4 Conclusion, 94
122 0 e p & ALL(b):[b e p => b+1 e p]
Join, 93, 121
As Required:
123 ALL(b):[b e n => b e p]
Detach, 43, 122
Prove: ALL(b):[b e n => pow(x,b+1)=pow'(x,b+1)]
Suppose...
124 y e n
Premise
125 y e n => y e p
U Spec, 123
126 y e p
Detach, 125, 124
Apply definition of p
127 y e p <=> y e n & pow(x,y+1)=pow'(x,y+1)
U Spec, 32
128 [y e p => y e n & pow(x,y+1)=pow'(x,y+1)]
& [y e n & pow(x,y+1)=pow'(x,y+1) => y e p]
Iff-And, 127
129 y e p => y e n & pow(x,y+1)=pow'(x,y+1)
Split, 128
130 y e n & pow(x,y+1)=pow'(x,y+1) => y e p
Split, 128
131 y e n & pow(x,y+1)=pow'(x,y+1)
Detach, 129, 126
132 y e n
Split, 131
133 pow(x,y+1)=pow'(x,y+1)
Split, 131
As Required:
134 ALL(b):[b e n => pow(x,b+1)=pow'(x,b+1)]
4 Conclusion, 124
As Required:
135 ALL(a):[a e n => ALL(b):[b e n => pow(a,b+1)=pow'(a,b+1)]]
4 Conclusion, 28
Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow'(a,b+1)]
Suppose...
136 x e n & y e n
Premise
137 x e n
Split, 136
138 y e n
Split, 136
Apply previous result
139 x e n => ALL(b):[b e n => pow(x,b+1)=pow'(x,b+1)]
U Spec, 135
140 ALL(b):[b e n => pow(x,b+1)=pow'(x,b+1)]
Detach, 139, 137
141 y e n => pow(x,y+1)=pow'(x,y+1)
U Spec, 140
142 pow(x,y+1)=pow'(x,y+1)
Detach, 141, 138
As Required:
143 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow'(a,b+1)]
4 Conclusion, 136
Prove: ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]
Suppose...
144 x e n & y e n
Premise
145 x e n
Split, 144
146 y e n
Split, 144
Prove: ~[x=0 & y=0] => pow(x,y)=pow'(x,y)
Suppose...
147 ~[x=0 & y=0]
Premise
148 ~~[~x=0 | ~y=0]
DeMorgan, 147
149 ~x=0 | ~y=0
Rem DNeg, 148
Prove: ~y=0 => pow(x,y)=pow'(x,y)
Suppose...
150 ~y=0
Premise
151 y e n => [~y=0 => EXIST(b):[b e n & b+1=y]]
U Spec, 7
152 ~y=0 => EXIST(b):[b e n & b+1=y]
Detach, 151, 146
153 EXIST(b):[b e n & b+1=y]
Detach, 152, 150
154 z e n & z+1=y
E Spec, 153
Define: z (the predecessor of y)
155 z e n
Split, 154
156 z+1=y
Split, 154
Apply definition of pow
157 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
158 x e n & z e n => pow(x,z+1)=pow(x,z)*x
U Spec, 157
159 x e n & z e n
Join, 145, 155
160 pow(x,z+1)=pow(x,z)*x
Detach, 158, 159
161 pow(x,y)=pow(x,z)*x
Substitute, 156, 160
Apply definition of pow'
162 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 16
163 x e n & z e n => pow'(x,z+1)=pow'(x,z)*x
U Spec, 162
164 pow'(x,z+1)=pow'(x,z)*x
Detach, 163, 159
165 pow'(x,y)=pow'(x,z)*x
Substitute, 156, 164
Two cases:
166 z=0 | ~z=0
Or Not
Prove: z=0 => pow(x,y)=pow'(x,y)
Suppose...
167 z=0
Premise
168 ALL(b):[x e n & b e n => pow(x,b+1)=pow'(x,b+1)]
U Spec, 143
169 x e n & z e n => pow(x,z+1)=pow'(x,z+1)
U Spec, 168
170 x e n & z e n
Join, 145, 155
171 pow(x,z+1)=pow'(x,z+1)
Detach, 169, 170
172 pow(x,y)=pow'(x,y)
Substitute, 156, 171
As Required:
173 z=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 167
Prove: ~z=0 => pow(x,y)=pow'(x,y)
Suppose...
174 ~z=0
Premise
Apply previous result
175 ALL(b):[x e n & b e n => pow(x,b+1)=pow'(x,b+1)]
U Spec, 143
176 x e n & z e n => pow(x,z+1)=pow'(x,z+1)
U Spec, 175
177 x e n & z e n
Join, 145, 155
178 pow(x,z+1)=pow'(x,z+1)
Detach, 176, 177
179 pow(x,y)=pow'(x,y)
Substitute, 156, 178
As Required:
180 ~z=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 174
181 [z=0 => pow(x,y)=pow'(x,y)]
& [~z=0 => pow(x,y)=pow'(x,y)]
Join, 173, 180
182 pow(x,y)=pow'(x,y)
Cases, 166, 181
As Required:
183 ~y=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 150
Prove: ~x=0 => pow(x,y)=pow'(x,y)
Suppose...
184 ~x=0
Premise
Apply Subset Axiom for proof by induction
185 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & pow(x,a)=pow'(x,a)]]
Subset, 1
186 Set(p) & ALL(a):[a e p <=> a e n & pow(x,a)=pow'(x,a)]
E Spec, 185
Define: p
*********
187 Set(p)
Split, 186
188 ALL(a):[a e p <=> a e n & pow(x,a)=pow'(x,a)]
Split, 186
189 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, 6
Prove: ALL(b):[b e p => b e n]
Suppose...
190 q e p
Premise
191 q e p <=> q e n & pow(x,q)=pow'(x,q)
U Spec, 188
192 [q e p => q e n & pow(x,q)=pow'(x,q)]
& [q e n & pow(x,q)=pow'(x,q) => q e p]
Iff-And, 191
193 q e p => q e n & pow(x,q)=pow'(x,q)
Split, 192
194 q e n & pow(x,q)=pow'(x,q) => q e p
Split, 192
195 q e n & pow(x,q)=pow'(x,q)
Detach, 193, 190
196 q e n
Split, 195
As Required:
197 ALL(b):[b e p => b e n]
4 Conclusion, 190
198 Set(p) & ALL(b):[b e p => b e n]
Join, 187, 197
Sufficient: ALL(b):[b e n => b e p]
199 0 e p & ALL(b):[b e p => b+1 e p]
=> ALL(b):[b e n => b e p]
Detach, 189, 198
Apply definition of p
200 0 e p <=> 0 e n & pow(x,0)=pow'(x,0)
U Spec, 188
201 [0 e p => 0 e n & pow(x,0)=pow'(x,0)]
& [0 e n & pow(x,0)=pow'(x,0) => 0 e p]
Iff-And, 200
202 0 e p => 0 e n & pow(x,0)=pow'(x,0)
Split, 201
Sufficient: 0 e p
203 0 e n & pow(x,0)=pow'(x,0) => 0 e p
Split, 201
204 x e n => [~x=0 => pow(x,0)=1]
U Spec, 11
205 ~x=0 => pow(x,0)=1
Detach, 204, 145
206 pow(x,0)=1
Detach, 205, 184
207 x e n => [~x=0 => pow'(x,0)=1]
U Spec, 15
208 ~x=0 => pow'(x,0)=1
Detach, 207, 145
209 pow'(x,0)=1
Detach, 208, 184
210 pow(x,0)=pow'(x,0)
Substitute, 209, 206
211 0 e n & pow(x,0)=pow'(x,0)
Join, 3, 210
As Required:
212 0 e p
Detach, 203, 211
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
213 q e p
Premise
Apply definition of p
214 q e p <=> q e n & pow(x,q)=pow'(x,q)
U Spec, 188
215 [q e p => q e n & pow(x,q)=pow'(x,q)]
& [q e n & pow(x,q)=pow'(x,q) => q e p]
Iff-And, 214
216 q e p => q e n & pow(x,q)=pow'(x,q)
Split, 215
217 q e n & pow(x,q)=pow'(x,q) => q e p
Split, 215
218 q e n & pow(x,q)=pow'(x,q)
Detach, 216, 213
219 q e n
Split, 218
220 pow(x,q)=pow'(x,q)
Split, 218
Apply definition of p
221 q+1 e p <=> q+1 e n & pow(x,q+1)=pow'(x,q+1)
U Spec, 188
222 [q+1 e p => q+1 e n & pow(x,q+1)=pow'(x,q+1)]
& [q+1 e n & pow(x,q+1)=pow'(x,q+1) => q+1 e p]
Iff-And, 221
223 q+1 e p => q+1 e n & pow(x,q+1)=pow'(x,q+1)
Split, 222
Sufficient: q+1 e p
224 q+1 e n & pow(x,q+1)=pow'(x,q+1) => q+1 e p
Split, 222
225 ALL(b):[q e n & b e n => q+b e n]
U Spec, 2
226 q e n & 1 e n => q+1 e n
U Spec, 225
227 q e n & 1 e n
Join, 219, 4
228 q+1 e n
Detach, 226, 227
Apply definition of pow
229 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
230 x e n & q e n => pow(x,q+1)=pow(x,q)*x
U Spec, 229
231 x e n & q e n
Join, 145, 219
232 pow(x,q+1)=pow(x,q)*x
Detach, 230, 231
Apply definition of pow'
233 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 16
234 x e n & q e n => pow'(x,q+1)=pow'(x,q)*x
U Spec, 233
235 pow'(x,q+1)=pow'(x,q)*x
Detach, 234, 231
236 pow'(x,q+1)=pow(x,q)*x
Substitute, 220, 235
237 pow(x,q+1)=pow'(x,q+1)
Substitute, 236, 232
238 q+1 e n & pow(x,q+1)=pow'(x,q+1)
Join, 228, 237
239 q+1 e p
Detach, 224, 238
As Required:
240 ALL(b):[b e p => b+1 e p]
4 Conclusion, 213
241 0 e p & ALL(b):[b e p => b+1 e p]
Join, 212, 240
As Required:
242 ALL(b):[b e n => b e p]
Detach, 199, 241
Prove: ALL(b):[b e n => pow(x,b)=pow'(x,b)]
Suppose...
243 q e n
Premise
244 q e n => q e p
U Spec, 242
245 q e p
Detach, 244, 243
Apply definition of p
246 q e p <=> q e n & pow(x,q)=pow'(x,q)
U Spec, 188
247 [q e p => q e n & pow(x,q)=pow'(x,q)]
& [q e n & pow(x,q)=pow'(x,q) => q e p]
Iff-And, 246
248 q e p => q e n & pow(x,q)=pow'(x,q)
Split, 247
249 q e n & pow(x,q)=pow'(x,q) => q e p
Split, 247
250 q e n & pow(x,q)=pow'(x,q)
Detach, 248, 245
251 q e n
Split, 250
252 pow(x,q)=pow'(x,q)
Split, 250
As Required:
253 ALL(b):[b e n => pow(x,b)=pow'(x,b)]
4 Conclusion, 243
254 y e n => pow(x,y)=pow'(x,y)
U Spec, 253
255 pow(x,y)=pow'(x,y)
Detach, 254, 146
As Required:
256 ~x=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 184
257 [~x=0 => pow(x,y)=pow'(x,y)]
& [~y=0 => pow(x,y)=pow'(x,y)]
Join, 256, 183
258 pow(x,y)=pow'(x,y)
Cases, 149, 257
As Required:
259 ~[x=0 & y=0] => pow(x,y)=pow'(x,y)
4 Conclusion, 147
As Required:
260 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]
4 Conclusion, 144
As Required:
261 ALL(pow):ALL(x0):ALL(pow'):ALL(x1):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
& pow'(0,0)=x1
& ALL(a):[a e n => [~a=0 => pow'(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]]
4 Conclusion, 8