(Commentary in dark blue font.
Statements in black, red and green font.)
INTRODUCTION
************
Here we present formal proof
that:
1. There exists infinitely many
binary functions ^ on the set of natural numbers N such that:
x^2 = x*x
x^(y+1) = x^y *
x
2. These functions differ ONLY
in the value assigned to 0^0.
This suggests that
exponentiation on N is indeterminate for 0^0.
THEOREM
*******
1. ALL(x0):[x0 e n
=> EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b)
e n]
& exp(0,0)=x0
& ALL(a):[a e n => exp(a,2)=a*a]
& ALL(a):ALL(b):[a
e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
2. 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 => exp(a,2)=a*a]
& 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 => exp'(a,2)=a*a]
& 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
3 1 e n
Axiom
Lemma 1 (Proof
here)
*******
For every x0 e n, there exists a binary function exp
on n such that:
exp(0,0) = x0
exp(x,1) = 1 for
~x =0
exp(x,y+1) = exp(x,y)
* x
4 ALL(x0):[x0 e n
=>
EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
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]]]
Axiom
Lemma 2 (Proof here)
*******
For every x0 e n, and binary function exp on n we
have:
exp(0,0) = x0
exp(x,1) = 1 for
~x =0
exp(x,y+1) = exp(x,y)
* x
if and only if...
exp(0,0) = x0
exp(x,2) = x * x
exp(x,y+1) = exp(x,y)
* x
5 ALL(x0):[x0 e n
=>
ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
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)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
Axiom
Lemma 3 (Proof here)
*******
For every x1, x2 e n, and binary functions exp and exp’ on n:
If
exp(0,0) = x1
exp(x,1) = 1 for
~x =0
exp(x,y+1) = exp(x,y)
* x
and
exp’(0,0) = x2
exp’(x,1) = 1 for
~x =0
exp’(x,y+1) = exp’(x,y)
* x
then
exp(x,y) = exp’(x,y) except for possibly when x = y = 0.
6 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)]]]]
Axiom
PROOF
*****
Prove: ALL(x0):[x0 e n
=> EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
& exp(0,0)=x0
& ALL(a):[a e n => exp(a,2)=a*a]
& ALL(a):ALL(b):[a
e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
Suppose...
7 x e n
Premise
Apply Lemma 1
8 x e n
=>
EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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]]
U Spec, 4
9 EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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]]
Detach, 8, 7
10 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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]
E Spec, 9
Apply Lemma 2
11 x e n
=>
ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
U Spec, 5
12 ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Detach, 11, 7
13 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
U Spec, 12
14 [ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=x
&
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]]
Iff-And, 13
15 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
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)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 14
16 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=x
&
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]
Split, 14
17 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Detach, 15, 10
As Required:
18 ALL(x0):[x0 e n
=>
EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
4 Conclusion, 7
Prove: 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 => exp(a,2)=a*a]
& 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 => exp'(a,2)=a*a]
& 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)]]]]
Suppose...
19 x1 e n & x2 e n
Premise
20 x1 e n
Split, 19
21 x2 e n
Split, 19
Suppose we have binary functions exp
and exp' such that..
22 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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 => exp'(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
Premise
We know from above that such functions exist in n:
Define: exp (with exp(0,0)=x1)
23 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 22
24 exp(0,0)=x1
Split, 22
25 ALL(a):[a e n => exp(a,2)=a*a]
Split, 22
26 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 22
Define: exp' (with exp'(0,0)=x2)
27 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
Split, 22
28 exp'(0,0)=x2
Split, 22
29 ALL(a):[a e n => exp'(a,2)=a*a]
Split, 22
30 ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
Split, 22
Apply Lemma 3
31 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)]]]]
U Spec, 6
32 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)]]]
U Spec, 31
33 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)]]]
Detach, 32, 19
34 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)]]]
U Spec, 33
35 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)]]
U Spec, 34
Apply Lemma 2 (for exp)
36 x1 e n
=>
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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
U Spec, 5
37 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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Detach, 36, 20
38 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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
U Spec, 37
39 [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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=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]]
Iff-And, 38
40 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)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 39
41 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
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)=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]
Split, 39
42 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x1
Join, 23, 24
43 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
Join, 42, 25
44 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x1
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Join, 43, 26
45 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]
Detach, 41, 44
Apply Lemma 2 (for exp')
46 x2 e n
=>
ALL(exp):[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 => exp(a,b) e n]
&
exp(0,0)=x2
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
U Spec, 5
47 ALL(exp):[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 => exp(a,b) e n]
&
exp(0,0)=x2
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Detach, 46, 21
48 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 => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
U Spec, 47
49 [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 => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
&
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 => exp'(a,2)=a*a]
&
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]]
Iff-And, 48
50 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 => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
Split, 49
51 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
&
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]
Split, 49
52 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
&
exp'(0,0)=x2
Join, 27, 28
53 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
Join, 52, 29
54 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
&
exp'(0,0)=x2
&
ALL(a):[a e n => exp'(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
Join, 53, 30
55 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]
Detach, 51, 54
56 ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]
Split, 55
57 exp'(0,0)=x2
Split, 55
58 ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
Split, 55
59 ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]
Split, 55
60 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]
Join, 45, 56
61 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
Join, 60, 57
62 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]]
Join, 61, 58
63 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]
Join, 62, 59
64 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]
Detach, 35, 63
As Required:
65 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 => exp(a,2)=a*a]
&
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 => exp'(a,2)=a*a]
&
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, 22
As Required:
66 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 => exp(a,2)=a*a]
&
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 => exp'(a,2)=a*a]
&
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, 19