THEOREM
*******
There exists a unique exponent
function on n with 0^0 left undefined.
Existence of exp(a,b):
EXIST(exp):[ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b) e n]]
& exp(0,1)=0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]
Uniqueness of exp(a,b):
ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b) e n]]
& exp(0,1)=0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n
=> [~[a=0 &
b=0] => 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) e n]]
& exp'(0,1)=0
& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n
=> [~[a=0 &
b=0] => 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 machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof.com
Dan Christensen
2019-10-17
AXIOMS/DEFINITIONS
******************
Define: n, 0, 1
***************
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
4 ~1=0
Axiom
5 0+1=1
Axiom
Properties of +
***************
Closed on n
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Adding 0
7 ALL(a):[a e n => a+0=a]
Axiom
+ Commutative
8 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
+ Right cancelable
9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b
=> a=c]]
Axiom
0 is "first" number
10 ALL(a):[a e n => ~a+1=0]
Axiom
Principle of Mathematical
Induction
11 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
Properties of *
***************
Closed on n
12 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
Multiplying by 0
13 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
14 ALL(a):[a e n => a*1=a]
Axiom
* Commutative
15 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Function Axiom (2 varibles)
**************
16 ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e f]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e f &
(a1,a2,b2) e f => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=>
(a1,a2,b) e f]]]]
Function
PREVIOUS RESULT
***************
There exists infinitely many
exponent-like functions starting with exponent 0 Proof
17 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
PROOF
*****
Suppose...
18 x0 e n
Premise
Apply previous result
19 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]]
U Spec, 17
20 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]]
Detach, 19, 18
21 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]
E Spec, 20
Define: exp
***********
22 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 21
23 exp(0,0)=x0
Split, 21
24 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 21
25 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 21
Construct n2
26 ALL(a1):ALL(a2):[Set(a1) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
27 ALL(a2):[Set(n) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 26
28 Set(n) & Set(n) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 27
29 Set(n) & Set(n)
Join, 1, 1
30 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 28, 29
31 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 30
Define: n2
32 Set'(n2)
Split, 31
33 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 31
Construct n3
34 ALL(a1):ALL(a2):ALL(a3):[Set(a1) &
Set(a2) & Set(a3) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]
Cart Prod
35 ALL(a2):ALL(a3):[Set(n) & Set(a2)
& Set(a3) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]
U Spec, 34
36 ALL(a3):[Set(n) & Set(n) & Set(a3)
=> EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]
U Spec, 35
37 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
U Spec, 36
38 Set(n) & Set(n)
Join, 1, 1
39 Set(n) & Set(n) & Set(n)
Join, 38, 1
40 EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
Detach, 37, 39
41 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 40
Define: n3
42 Set''(n3)
Split, 41
43 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 41
Construct dom
44 EXIST(sub):[Set'(sub) &
ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]
Subset, 32
45 Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]
E Spec, 44
Define: dom
46 Set'(dom)
Split, 45
47 ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]
Split, 45
Construct exp'
48 EXIST(sub):[Set''(sub) &
ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]]
Subset, 42
49 Set''(exp') & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]
E Spec, 48
Define: exp'
************
50 Set''(exp')
Split, 49
51 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]
Split, 49
Apply Function Axioms (for 2 variables)
52 ALL(f):ALL(dom):ALL(cod):[Set''(f) &
Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e f]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e f &
(a1,a2,b2) e f => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=>
(a1,a2,b) e f]]]]
Function
53 ALL(dom):ALL(cod):[Set''(exp') &
Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]]
U Spec, 52
54 ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]]
U Spec, 53
55 Set''(exp') & Set'(dom) & Set(n)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]
U Spec, 54
56 Set''(exp') & Set'(dom)
Join, 50, 46
57 Set''(exp') & Set'(dom) & Set(n)
Join, 56, 1
Sufficient: For functionality of exp'
58 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]
Detach, 55, 57
Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b)
e exp' => (a1,a2) e dom & b e n]
Suppose...
59 (x,y,z) e exp'
Premise
Apply definition of exp'
60 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
61 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 60
62 (x,y,z) e exp'
<=>
(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
U Spec, 61
63 [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]
&
[(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']
Iff-And, 62
64 (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Split, 63
65 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'
Split, 63
66 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Detach, 64, 59
67 (x,y,z) e n3
Split, 66
68 ~[x=0 & y=0] & z=exp(x,y)
Split, 66
69 ~[x=0 & y=0]
Split, 68
70 z=exp(x,y)
Split, 68
71 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
72 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 71
73 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 72
74 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 73
Apply definition of n3
75 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
76 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 75
77 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 76
78 [(x,y,z) e n3 => x e n & y e n & z e n]
&
[x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 77
79 (x,y,z) e n3 => x e n & y e n & z e n
Split, 78
80 x e n & y e n & z e n => (x,y,z) e n3
Split, 78
81 x e n & y e n & z e n
Detach, 79, 67
82 x e n
Split, 81
83 y e n
Split, 81
84 z e n
Split, 81
Sufficient: For (x,y) e dom
85 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 73
Apply definition of n3
86 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
87 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 86
88 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 87
89 [(x,y,z) e n3 => x e n & y e n & z e n]
&
[x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 88
90 (x,y,z) e n3 => x e n & y e n & z e n
Split, 89
91 x e n & y e n & z e n => (x,y,z) e n3
Split, 89
92 x e n & y e n & z e n
Detach, 90, 67
93 x e n
Split, 92
94 y e n
Split, 92
95 z e n
Split, 92
Apply definition of n2
96 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
97 (x,y) e n2 <=> x e n & y e n
U Spec, 96
98 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 97
99 (x,y) e n2 => x e n & y e n
Split, 98
100 x e n & y e n => (x,y) e n2
Split, 98
101 x e n & y e n
Join, 82, 83
102 (x,y) e n2
Detach, 100, 101
103 (x,y) e n2 & ~[x=0 & y=0]
Join, 102, 69
104 (x,y) e dom
Detach, 85, 103
105 (x,y) e dom & z e n
Join, 104, 84
Functionality of exp', Part 1
106 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
4 Conclusion, 59
Prove: ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n &
(a1,a2,b) e exp']]
Suppose...
107 (x,y) e dom
Premise
Apply definition of dom
108 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
109 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 108
110 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 109
111 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 110
112 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 110
113 (x,y) e n2 & ~[x=0 & y=0]
Detach, 111, 107
114 (x,y) e n2
Split, 113
115 ~[x=0 & y=0]
Split, 113
Apply definition of exp'
116 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
117 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 116
118 ALL(b):[x e n & b e n => exp(x,b) e n]
U Spec, 22
119 x e n & y e n => exp(x,y) e n
U Spec, 118
Apply definition of n2
120 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
121 (x,y) e n2 <=> x e n & y e n
U Spec, 120
122 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 121
123 (x,y) e n2 => x e n & y e n
Split, 122
124 x e n & y e n => (x,y) e n2
Split, 122
125 x e n & y e n
Detach, 123, 114
126 x e n
Split, 125
127 y e n
Split, 125
128 exp(x,y) e n
Detach, 119, 125
129 (x,y,exp(x,y)) e exp'
<=>
(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]
U Spec, 117, 128
130 [(x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]]
&
[(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp']
Iff-And, 129
131 (x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]
Split, 130
Sufficient: For (x,y,exp(x,y)) e exp'
132 (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp'
Split, 130
Apply definition of n3
133 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
134 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 133
135 (x,y,exp(x,y)) e n3 <=> x e n & y e n & exp(x,y) e n
U Spec, 134, 128
136 [(x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n]
&
[x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3]
Iff-And, 135
137 (x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n
Split, 136
Sufficient: For (x,y,exp(x,y)) e n3
138 x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3
Split, 136
139 x e n & y e n & exp(x,y) e n
Join, 125, 128
140 (x,y,exp(x,y)) e n3
Detach, 138, 139
141 exp(x,y)=exp(x,y)
Reflex, 128
142 ~[x=0 & y=0] & exp(x,y)=exp(x,y)
Join, 115, 141
143 (x,y,exp(x,y)) e n3
&
[~[x=0 & y=0] & exp(x,y)=exp(x,y)]
Join, 140, 142
144 (x,y,exp(x,y)) e exp'
Detach, 132, 143
145 exp(x,y) e n & (x,y,exp(x,y)) e exp'
Join, 128, 144
146 EXIST(b):[b e n & (x,y,b) e exp']
E Gen, 145
Functionality of exp', Part 2
147 ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]
4 Conclusion, 107
Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2)
e dom & b1 e n & b2 e n
=> [(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
Suppose...
148 (x,y) e dom & z1 e n & z2 e n
Premise
149 (x,y) e dom
Split, 148
150 z1 e n
Split, 148
151 z2 e n
Split, 148
Suppose...
152 (x,y,z1) e exp' & (x,y,z2) e exp'
Premise
153 (x,y,z1) e exp'
Split, 152
154 (x,y,z2) e exp'
Split, 152
Apply the definition of exp'
155 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
156 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 155
157 (x,y,z1) e exp'
<=>
(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
U Spec, 156
158 [(x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]]
&
[(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp']
Iff-And, 157
159 (x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
Split, 158
160 (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp'
Split, 158
161 (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
Detach, 159, 153
162 (x,y,z1) e n3
Split, 161
163 ~[x=0 & y=0] & z1=exp(x,y)
Split, 161
164 ~[x=0 & y=0]
Split, 163
165 z1=exp(x,y)
Split, 163
166 (x,y,z2) e exp'
<=>
(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
U Spec, 156
167 [(x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]]
&
[(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp']
Iff-And, 166
168 (x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
Split, 167
169 (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp'
Split, 167
170 (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
Detach, 168, 154
171 (x,y,z2) e n3
Split, 170
172 ~[x=0 & y=0] & z2=exp(x,y)
Split, 170
173 ~[x=0 & y=0]
Split, 172
174 z2=exp(x,y)
Split, 172
175 z1=z2
Substitute, 174,
165
176 (x,y,z1) e exp' & (x,y,z2) e exp' => z1=z2
4 Conclusion, 152
Functionality of exp', Part 3
177 ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
4 Conclusion, 148
Joining results...
178 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
Join, 106, 147
179 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
Join, 178, 177
exp' is a partial binary function on n
As Required:
180 ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]
Detach, 58, 179
Prove: ALL(x):ALL(y):[x e n & y e n =>
[~[x=0 & y=0] => exp'(x,y) e n]]
Suppose...
181 x e n & y e n
Premise
Prove: ~[x=0 & y=0] => exp'(x,y)
e n
Suppose...
182 ~[x=0 & y=0]
Premise
Apply definition of exp'
183 ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]
U Spec, 147
184 (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']
U Spec, 183
Apply definition of dom
185 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
186 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 185
187 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 186
188 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 187
189 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 187
Apply definition of n2
190 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
191 (x,y) e n2 <=> x e n & y e n
U Spec, 190
192 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 191
193 (x,y) e n2 => x e n & y e n
Split, 192
194 x e n & y e n => (x,y) e n2
Split, 192
195 (x,y) e n2
Detach, 194, 181
196 (x,y) e n2 & ~[x=0 & y=0]
Join, 195, 182
197 (x,y) e dom
Detach, 189, 196
198 EXIST(b):[b e n & (x,y,b) e exp']
Detach, 184, 197
199 z e n & (x,y,z) e exp'
E Spec, 198
200 z e n
Split, 199
201 (x,y,z) e exp'
Split, 199
Apply previous result
202 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
203 ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]
U Spec, 202
204 (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']
U Spec, 203
205 (x,y) e dom & z e n
Join, 197, 200
206 exp'(x,y)=z <=> (x,y,z) e exp'
Detach, 204, 205
207 [exp'(x,y)=z => (x,y,z) e exp']
&
[(x,y,z) e exp' => exp'(x,y)=z]
Iff-And, 206
208 exp'(x,y)=z => (x,y,z) e exp'
Split, 207
209 (x,y,z) e exp' => exp'(x,y)=z
Split, 207
210 exp'(x,y)=z
Detach, 209, 201
211 exp'(x,y) e n
Substitute, 210,
200
As Required:
212 ~[x=0 & y=0] => exp'(x,y) e n
4 Conclusion, 182
As Required:
213 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
4 Conclusion, 181
Prove: exp'(0,1)=0
Apply definition of exp'
214 ALL(b):ALL(c):[(0,b,c) e exp'
<=>
(0,b,c) e n3 & [~[0=0 & b=0] & c=exp(0,b)]]
U Spec, 51
215 ALL(c):[(0,1,c) e exp'
<=>
(0,1,c) e n3 & [~[0=0 & 1=0] & c=exp(0,1)]]
U Spec, 214
216 (0,1,0) e exp'
<=>
(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
U Spec, 215
217 [(0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]]
&
[(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp']
Iff-And, 216
218 (0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
Split, 217
Sufficient: For (0,1,0) e exp'
219 (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp'
Split, 217
Apply definition of n3
220 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 43
221 ALL(c3):[(0,1,c3) e n3 <=> 0 e n & 1 e n & c3 e n]
U Spec, 220
222 (0,1,0) e n3 <=> 0 e n & 1 e n & 0 e n
U Spec, 221
223 [(0,1,0) e n3 => 0 e n & 1 e n & 0 e n]
&
[0 e n & 1 e n & 0 e n => (0,1,0) e n3]
Iff-And, 222
224 (0,1,0) e n3 => 0 e n & 1 e n & 0 e n
Split, 223
225 0 e n & 1 e n & 0 e n => (0,1,0) e n3
Split, 223
226 0 e n & 1 e n
Join, 2, 3
227 0 e n & 1 e n & 0 e n
Join, 226, 2
228 (0,1,0) e n3
Detach, 225, 227
Prove: ~[0=0 & 1=0]
Suppose to the contrary...
229 0=0 & 1=0
Premise
230 0=0
Split, 229
231 1=0
Split, 229
232 1=0 & ~1=0
Join, 231, 4
233 ~[0=0 & 1=0]
4 Conclusion, 229
Apply definition of exp
234 ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]
U Spec, 25
235 0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0
U Spec, 234
236 0 e n & 0 e n
Join, 2, 2
237 exp(0,0+1)=exp(0,0)*0
Detach, 235, 236
238 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 8
239 0 e n & 1 e n => 0+1=1+0
U Spec, 238
240 0 e n & 1 e n
Join, 2, 3
241 0+1=1+0
Detach, 239, 240
242 1 e n => 1+0=1
U Spec, 7
243 1+0=1
Detach, 242, 3
244 0+1=1
Substitute, 243,
241
245 exp(0,1)=exp(0,0)*0
Substitute, 244,
237
246 ALL(b):[0 e n & b e n => exp(0,b) e n]
U Spec, 22
247 0 e n & 0 e n => exp(0,0) e n
U Spec, 246
248 0 e n & 0 e n
Join, 2, 2
249 exp(0,0) e n
Detach, 247, 248
250 exp(0,0) e n => exp(0,0)*0=0
U Spec, 13, 249
251 exp(0,0)*0=0
Detach, 250, 249
252 exp(0,1)=0
Substitute, 251,
245
253 0=exp(0,1)
Sym, 252
254 ~[0=0 & 1=0] & 0=exp(0,1)
Join, 233, 253
255 (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
Join, 228, 254
256 (0,1,0) e exp'
Detach, 219, 255
Apply previous result
257 ALL(a2):ALL(b):[(0,a2) e dom & b e n => [exp'(0,a2)=b <=>
(0,a2,b) e exp']]
U Spec, 180
258 ALL(b):[(0,1) e dom & b e n => [exp'(0,1)=b <=> (0,1,b) e exp']]
U Spec, 257
259 (0,1) e dom & 0 e n => [exp'(0,1)=0 <=> (0,1,0) e exp']
U Spec, 258
Apply defintion of dom
260 ALL(b):[(0,b) e dom <=> (0,b) e n2 & ~[0=0 & b=0]]
U Spec, 47
261 (0,1) e dom <=> (0,1) e n2 & ~[0=0 & 1=0]
U Spec, 260
262 [(0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]]
&
[(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom]
Iff-And, 261
263 (0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]
Split, 262
264 (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom
Split, 262
265 ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]
U Spec, 33
266 (0,1) e n2 <=> 0 e n & 1 e n
U Spec, 265
267 [(0,1) e n2 => 0 e n & 1 e n]
&
[0 e n & 1 e n => (0,1) e n2]
Iff-And, 266
268 (0,1) e n2 => 0 e n & 1 e n
Split, 267
269 0 e n & 1 e n => (0,1) e n2
Split, 267
270 0 e n & 1 e n
Join, 2, 3
271 (0,1) e n2
Detach, 269, 270
272 0=0 & 1=0
Premise
273 0=0
Split, 272
274 1=0
Split, 272
275 1=0 & ~1=0
Join, 274, 4
276 ~[0=0 & 1=0]
4 Conclusion, 272
277 (0,1) e n2 & ~[0=0 & 1=0]
Join, 271, 276
278 (0,1) e dom
Detach, 264, 277
279 (0,1) e dom & 0 e n
Join, 278, 2
280 exp'(0,1)=0 <=> (0,1,0) e exp'
Detach, 259, 279
281 [exp'(0,1)=0 => (0,1,0) e exp']
&
[(0,1,0) e exp' => exp'(0,1)=0]
Iff-And, 280
282 exp'(0,1)=0 => (0,1,0) e exp'
Split, 281
283 (0,1,0) e exp' => exp'(0,1)=0
Split, 281
As Required:
284 exp'(0,1)=0
Detach, 283, 256
Prove: ALL(a):[a e n => [~x=0 => exp'(x,0)=1]]
Suppose...
285 x e n
Premise
Prove: ~x=0 => exp'(x,0)=1
Suppose...
286 ~x=0
Premise
287 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
288 ALL(c):[(x,0,c) e exp'
<=>
(x,0,c) e n3 & [~[x=0 & 0=0] & c=exp(x,0)]]
U Spec, 287
289 (x,0,1) e exp'
<=>
(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
U Spec, 288
290 [(x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]]
&
[(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp']
Iff-And, 289
291 (x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
Split, 290
Sufficient: For (x,0,1) e exp'
292 (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp'
Split, 290
Apply definition of n3
293 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
294 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 293
295 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n
U Spec, 294
296 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]
&
[x e n & 0 e n & 1 e n => (x,0,1) e n3]
Iff-And, 295
297 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]
&
[x e n & 0 e n & 1 e n => (x,0,1) e n3]
Iff-And, 295
298 (x,0,1) e n3 => x e n & 0 e n & 1 e n
Split, 297
299 x e n & 0 e n & 1 e n => (x,0,1) e n3
Split, 297
300 x e n & 0 e n
Join, 285, 2
301 x e n & 0 e n & 1 e n
Join, 300, 3
302 (x,0,1) e n3
Detach, 299, 301
303 x=0 & 0=0
Premise
304 x=0
Split, 303
305 0=0
Split, 303
306 x=0 & ~x=0
Join, 304, 286
307 ~[x=0 & 0=0]
4 Conclusion, 303
Apply definition of exp
308 x e n => [~x=0 => exp(x,0)=1]
U Spec, 24
309 ~x=0 => exp(x,0)=1
Detach, 308, 285
310 exp(x,0)=1
Detach, 309, 286
311 1=exp(x,0)
Sym, 310
312 ~[x=0 & 0=0] & 1=exp(x,0)
Join, 307, 311
313 (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
Join, 302, 312
314 (x,0,1) e exp'
Detach, 292, 313
315 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
316 ALL(b):[(x,0) e dom & b e n => [exp'(x,0)=b <=> (x,0,b) e exp']]
U Spec, 315
317 (x,0) e dom & 1 e n => [exp'(x,0)=1 <=> (x,0,1) e exp']
U Spec, 316
Apply definition of dom
318 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
319 (x,0) e dom <=> (x,0) e n2 & ~[x=0 & 0=0]
U Spec, 318
320 [(x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]]
&
[(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom]
Iff-And, 319
321 (x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]
Split, 320
322 (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom
Split, 320
Apply definition of n2
323 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
324 (x,0) e n2 <=> x e n & 0 e n
U Spec, 323
325 [(x,0) e n2 => x e n & 0 e n]
&
[x e n & 0 e n => (x,0) e n2]
Iff-And, 324
326 (x,0) e n2 => x e n & 0 e n
Split, 325
327 x e n & 0 e n => (x,0) e n2
Split, 325
328 x e n & 0 e n
Join, 285, 2
329 (x,0) e n2
Detach, 327, 328
330 x=0 & 0=0
Premise
331 x=0
Split, 330
332 0=0
Split, 330
333 x=0 & ~x=0
Join, 331, 286
334 ~[x=0 & 0=0]
4 Conclusion, 330
335 (x,0) e n2 & ~[x=0 & 0=0]
Join, 329, 334
336 (x,0) e dom
Detach, 322, 335
337 (x,0) e dom & 1 e n
Join, 336, 3
338 exp'(x,0)=1 <=> (x,0,1) e exp'
Detach, 317, 337
339 [exp'(x,0)=1 => (x,0,1) e exp']
&
[(x,0,1) e exp' => exp'(x,0)=1]
Iff-And, 338
340 exp'(x,0)=1 => (x,0,1) e exp'
Split, 339
341 (x,0,1) e exp' => exp'(x,0)=1
Split, 339
342 exp'(x,0)=1
Detach, 341, 314
As Required:
343 ~x=0 => exp'(x,0)=1
4 Conclusion, 286
As Required:
344 ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
4 Conclusion, 285
Prove: ALL(a):ALL(b):[a e n & b e n =>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]
Suppose...
345 x e n & y e n
Premise
346 x e n
Split, 345
347 y e n
Split, 345
Prove: ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x
Suppose...
348 ~[x=0 & y=0]
Premise
Apply previous result
349 ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]
U Spec, 147
350 (x,y) e dom =>
EXIST(b):[b e n & (x,y,b) e exp']
U Spec, 349
Apply definition of dom
351 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
352 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 351
353 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 352
354 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 353
355 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 353
Apply definition of n2
356 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
357 (x,y) e n2 <=> x e n & y e n
U Spec, 356
358 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 357
359 (x,y) e n2 => x e n & y e n
Split, 358
360 x e n & y e n => (x,y) e n2
Split, 358
361 (x,y) e n2
Detach, 360, 345
362 (x,y) e n2 & ~[x=0 & y=0]
Join, 361, 348
363 (x,y) e dom
Detach, 355, 362
364 EXIST(b):[b e n & (x,y,b) e exp']
Detach, 350, 363
365 z e n & (x,y,z) e exp'
E Spec, 364
366 z e n
Split, 365
367 (x,y,z) e exp'
Split, 365
368 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
369 ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]
U Spec, 368
370 (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']
U Spec, 369
371 ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]
U Spec, 368
372 (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']
U Spec, 371
373 (x,y) e dom & z e n
Join, 363, 366
374 exp'(x,y)=z <=> (x,y,z) e exp'
Detach, 372, 373
375 [exp'(x,y)=z => (x,y,z) e exp']
&
[(x,y,z) e exp' => exp'(x,y)=z]
Iff-And, 374
376 exp'(x,y)=z => (x,y,z) e exp'
Split, 375
377 (x,y,z) e exp' => exp'(x,y)=z
Split, 375
378 exp'(x,y)=z
Detach, 377, 367
379 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
380 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 379
381 (x,y,z) e exp'
<=>
(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
U Spec, 380
382 [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]
&
[(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']
Iff-And, 381
383 (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Split, 382
384 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'
Split, 382
385 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Detach, 383, 367
386 (x,y,z) e n3
Split, 385
387 ~[x=0 & y=0] & z=exp(x,y)
Split, 385
388 ~[x=0 & y=0]
Split, 387
389 z=exp(x,y)
Split, 387
390 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
391 y e n & 1 e n => y+1 e n
U Spec, 390
392 y e n & 1 e n
Join, 347, 3
393 y+1 e n
Detach, 391, 392
394 ALL(b):[z e n & b e n => z*b e n]
U Spec, 12
395 z e n & x e n => z*x e n
U Spec, 394
396 z e n & x e n
Join, 366, 346
397 z*x e n
Detach, 395, 396
Apply definition of exp'
398 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
399 ALL(c):[(x,y+1,c) e exp'
<=>
(x,y+1,c) e n3 & [~[x=0 & y+1=0] & c=exp(x,y+1)]]
U Spec, 398, 393
400 (x,y+1,z*x) e exp'
<=>
(x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]
U Spec, 399, 397
401 [(x,y+1,z*x) e exp' => (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]]
&
[(x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)] => (x,y+1,z*x) e exp']
Iff-And, 400
402 (x,y+1,z*x) e exp' => (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]
Split, 401
403 (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)] => (x,y+1,z*x) e exp'
Split, 401
404 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
405 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]
U Spec, 404, 393
406 (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n
U Spec, 405, 397
407 [(x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n]
&
[x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3]
Iff-And, 406
408 (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n
Split, 407
409 x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3
Split, 407
410 x e n & y+1 e n
Join, 346, 393
411 x e n & y+1 e n & z*x e n
Join, 410, 397
412 (x,y+1,z*x) e n3
Detach, 409, 411
Prove: ~[x=0 & y+1=0]
Suppose to the contrary...
413 x=0 & y+1=0
Premise
414 x=0
Split, 413
415 y+1=0
Split, 413
416 y e n => ~y+1=0
U Spec, 10
417 ~y+1=0
Detach, 416, 347
418 y+1=0 & ~y+1=0
Join, 415, 417
As Required:
419 ~[x=0 & y+1=0]
4 Conclusion, 413
420 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 25
421 x e n & y e n => exp(x,y+1)=exp(x,y)*x
U Spec, 420
422 exp(x,y+1)=exp(x,y)*x
Detach, 421, 345
423 exp(x,y+1)=z*x
Substitute, 389,
422
424 z*x=exp(x,y+1)
Sym, 423
425 ~[x=0 & y+1=0] & z*x=exp(x,y+1)
Join, 419, 424
426 (x,y+1,z*x) e n3
&
[~[x=0 & y+1=0] & z*x=exp(x,y+1)]
Join, 412, 425
427 (x,y+1,z*x) e exp'
Detach, 403, 426
428 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
429 ALL(b):[(x,y+1) e dom & b e n => [exp'(x,y+1)=b <=> (x,y+1,b) e exp']]
U Spec, 428, 393
430 (x,y+1) e dom & z*x e n => [exp'(x,y+1)=z*x <=> (x,y+1,z*x) e exp']
U Spec, 429, 397
431 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
432 (x,y+1) e dom <=> (x,y+1) e n2 & ~[x=0 & y+1=0]
U Spec, 431, 393
433 [(x,y+1) e dom => (x,y+1) e n2 & ~[x=0 & y+1=0]]
&
[(x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e dom]
Iff-And, 432
434 (x,y+1) e dom => (x,y+1) e n2 & ~[x=0 & y+1=0]
Split, 433
435 (x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e dom
Split, 433
436 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
437 (x,y+1) e n2 <=> x e n & y+1 e n
U Spec, 436, 393
438 [(x,y+1) e n2 => x e n & y+1 e n]
&
[x e n & y+1 e n => (x,y+1) e n2]
Iff-And, 437
439 (x,y+1) e n2 => x e n & y+1 e n
Split, 438
440 x e n & y+1 e n => (x,y+1) e n2
Split, 438
441 x e n & y+1 e n
Join, 346, 393
442 (x,y+1) e n2
Detach, 440, 441
443 (x,y+1) e n2 & ~[x=0 & y+1=0]
Join, 442, 419
444 (x,y+1) e dom
Detach, 435, 443
445 (x,y+1) e dom & z*x e n
Join, 444, 397
446 exp'(x,y+1)=z*x <=> (x,y+1,z*x) e exp'
Detach, 430, 445
447 [exp'(x,y+1)=z*x => (x,y+1,z*x) e exp']
&
[(x,y+1,z*x) e exp' => exp'(x,y+1)=z*x]
Iff-And, 446
448 exp'(x,y+1)=z*x => (x,y+1,z*x) e exp'
Split, 447
449 (x,y+1,z*x) e exp' => exp'(x,y+1)=z*x
Split, 447
450 exp'(x,y+1)=z*x
Detach, 449, 427
451 exp'(x,y+1)=exp'(x,y)*x
Substitute, 378,
450
As Required:
452 ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x
4 Conclusion, 348
As Required:
453 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]
4 Conclusion, 345
454 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
&
exp'(0,1)=0
Join, 213, 284
455 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
&
exp'(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
Join, 454, 344
456 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
&
exp'(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]
Join, 455, 453
As Required:
457 ALL(x0):[x0 e n
=>
EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
&
exp(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]]
4 Conclusion, 18
458 0 e n
=>
EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
&
exp(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]
U Spec, 457
As Required:
459 EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
&
exp(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]
Detach, 458, 2
Prove the exp function is unique
Suppose...
460 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
&
exp(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => 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) e n]]
&
exp'(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]
Premise
Define: exp
461 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
Split, 460
462 exp(0,1)=0
Split, 460
463 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 460
464 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]
Split, 460
465 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
&
exp'(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]
Split, 460
Define: exp'
466 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
Split, 465
467 exp'(0,1)=0
Split, 465
468 ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
Split, 465
469 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]
Split, 465
Prove: ALL(a):[a e n
=> ALL(b):[b e n => [~[a=0 & b=0] =>
exp(a,b)=exp'(a,b)]]]
Suppose...
470 x e n
Premise
Two cases to consider:
471 x=0 | ~x=0
Or Not
Construct subset p of n
Apply Subset Axiom
472 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]]
Subset, 1
473 Set(p) & ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
E Spec, 472
Define: p
474 Set(p)
Split, 473
475 ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
Split, 473
Apply Principle of Mathematical Induction
476 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, 11
Prove p is a subset of n
Suppose...
477 y e p
Premise
Apply definition of p
478 y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
U Spec, 475
479 [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]
&
[y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]
Iff-And, 478
480 y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Split, 479
481 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p
Split, 479
482 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Detach, 480, 477
483 y e n
Split, 482
As Required:
484 ALL(b):[b e p => b e n]
4 Conclusion, 477
485 Set(p) & ALL(b):[b e p => b e n]
Join, 474, 484
Sufficient: For ALL(b):[b e n => b e p]
486 0 e p & ALL(b):[b e p => b+1 e p]
=>
ALL(b):[b e n => b e p]
Detach, 476, 485
Base Case
*********
Apply definiton of p
487 0 e p <=> 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]
U Spec, 475
488 [0 e p => 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]]
&
[0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)] => 0 e p]
Iff-And, 487
489 0 e p => 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]
Split, 488
Sufficient: For 0 e p
490 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)] => 0 e p
Split, 488
491 0 e n & [~~[x=0 & 0=0] | exp(x,0)=exp'(x,0)] => 0 e p
Imply-Or, 490
492 0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)] => 0 e p
Rem DNeg, 491
Case 1
Prove: x=0 => 0 e p
Suppose...
493 x=0
Premise
494 0=0
Reflex
495 x=0 & 0=0
Join, 493, 494
496 x=0 & 0=0 | exp(x,0)=exp'(x,0)
Arb Or, 495
497 0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)]
Join, 2, 496
498 0 e p
Detach, 492, 497
Case 1
As Required:
499 x=0 => 0 e p
4 Conclusion, 493
Case 2
Prove: ~x=0 => 0 e p
Suppose...
500 ~x=0
Premise
Apply definition of exp
501 x e n => [~x=0 => exp(x,0)=1]
U Spec, 463
502 ~x=0 => exp(x,0)=1
Detach, 501, 470
503 exp(x,0)=1
Detach, 502, 500
504 x e n => [~x=0 => exp'(x,0)=1]
U Spec, 468
505 ~x=0 => exp'(x,0)=1
Detach, 504, 470
506 exp'(x,0)=1
Detach, 505, 500
507 exp(x,0)=exp'(x,0)
Substitute, 506,
503
508 x=0 & 0=0 | exp(x,0)=exp'(x,0)
Arb Or, 507
509 0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)]
Join, 2, 508
510 0 e p
Detach, 492, 509
Case 2
As Required:
511 ~x=0 => 0 e p
4 Conclusion, 500
512 [x=0 => 0 e p] & [~x=0 => 0 e p]
Join, 499, 511
Apply Cases Rule
As Required:
513 0 e p
Cases, 471, 512
Inductive Step
**************
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
514 y e p
Premise
Two sub-cases to consider:
515 y=0 | ~y=0
Or Not
Apply definition of p
516 y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
U Spec, 475
517 [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]
&
[y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]
Iff-And, 516
518 y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Split, 517
519 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p
Split, 517
520 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Detach, 518, 514
521 y e n
Split, 520
522 ~[x=0 & y=0] => exp(x,y)=exp'(x,y)
Split, 520
523 ~~[x=0 & y=0] | exp(x,y)=exp'(x,y)
Imply-Or, 522
524 x=0 & y=0 | exp(x,y)=exp'(x,y)
Rem DNeg, 523
525 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
526 y e n & 1 e n => y+1 e n
U Spec, 525
527 y e n & 1 e n
Join, 521, 3
528 y+1 e n
Detach, 526, 527
Apply definition of p
529 y+1 e p <=> y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]
U Spec, 475, 528
530 [y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]]
&
[y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)] => y+1 e p]
Iff-And, 529
531 y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]
Split, 530
Sufficient: For y+1 e p
532 y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)] => y+1 e p
Split, 530
533 y+1 e n & [~~[x=0 & y+1=0] | exp(x,y+1)=exp'(x,y+1)] => y+1 e p
Imply-Or, 532
534 y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)] => y+1 e p
Rem DNeg, 533
Case 1
Prove: x=0 => y+1 e p
Suppose...
535 x=0
Premise
Sub-case 1
Prove: y=0 => y+1 e p
Suppose...
536 y=0
Premise
537 y+1 e n & [0=0 & y+1=0 | exp(0,y+1)=exp'(0,y+1)] => y+1 e p
Substitute, 535,
534
538 y+1 e n & [0=0 & 0+1=0 | exp(0,0+1)=exp'(0,0+1)] => y+1 e p
Substitute, 536,
537
539 y+1 e n & [0=0 & 1=0 | exp(0,1)=exp'(0,1)] => y+1 e p
Substitute, 5,
538
540 exp(0,1)=exp'(0,1)
Substitute, 467,
462
541 0=0 & 1=0 | exp(0,1)=exp'(0,1)
Arb Or, 540
542 y+1 e n & [0=0 & 1=0 | exp(0,1)=exp'(0,1)]
Join, 528, 541
543 y+1 e p
Detach, 539, 542
Sub-case 1
As Required:
544 y=0 => y+1 e p
4 Conclusion, 536
Sub-case 2
Prove: ~y=0 => y+1 e p
Suppose...
545 ~y=0
Premise
546 y+1 e n & [0=0 & y+1=0 | exp(0,y+1)=exp'(0,y+1)] => y+1 e p
Substitute, 535,
534
Prove: ~[x=0 &
y=0]
Suppose to the contrary...
547 x=0 & y=0
Premise
548 x=0
Split, 547
549 y=0
Split, 547
550 y=0 & ~y=0
Join, 549, 545
As Required:
551 ~[x=0 & y=0]
4 Conclusion, 547
552 exp(x,y)=exp'(x,y)
Detach, 522, 551
Apply definition of exp
553 ALL(b):[x e n & b e n
=>
[~[x=0 & b=0] => exp(x,b+1)=exp(x,b)*x]]
U Spec, 464
554 x e n & y e n
=>
[~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x]
U Spec, 553
555 x e n & y e n
Join, 470, 521
556 ~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x
Detach, 554, 555
557 exp(x,y+1)=exp(x,y)*x
Detach, 556, 551
Apply definition of exp'
558 ALL(b):[x e n & b e n
=>
[~[x=0 & b=0] => exp'(x,b+1)=exp'(x,b)*x]]
U Spec, 469
559 x e n & y e n
=>
[~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x]
U Spec, 558
560 ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x
Detach, 559, 555
561 exp'(x,y+1)=exp'(x,y)*x
Detach, 560, 551
562 exp'(x,y+1)=exp(x,y)*x
Substitute, 552,
561
563 exp(x,y+1)=exp'(x,y+1)
Substitute, 562,
557
564 x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)
Arb Or, 563
565 y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)]
Join, 528, 564
566 y+1 e p
Detach, 534, 565
Sub-case 2
As Required:
567 ~y=0 => y+1 e p
4 Conclusion, 545
568 [y=0 => y+1 e p] & [~y=0 => y+1 e p]
Join, 544, 567
569 y+1 e p
Cases, 515, 568
Case 1
As Required:
570 x=0 => y+1 e p
4 Conclusion, 535
Case 2
Prove: ~x=0 => y+1 e p
Suppose...
571 ~x=0
Premise
Prove: ~[x=0 &
y=0]
Suppose to the contrary...
572 x=0 & y=0
Premise
573 x=0
Split, 572
574 y=0
Split, 572
575 x=0 & ~x=0
Join, 573, 571
As Required:
576 ~[x=0 & y=0]
4 Conclusion, 572
577 exp(x,y)=exp'(x,y)
Detach, 522, 576
Apply definition of exp
578 ALL(b):[x e n & b e n
=>
[~[x=0 & b=0] => exp(x,b+1)=exp(x,b)*x]]
U Spec, 464
579 x e n & y e n
=>
[~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x]
U Spec, 578
580 x e n & y e n
Join, 470, 521
581 ~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x
Detach, 579, 580
582 exp(x,y+1)=exp(x,y)*x
Detach, 581, 576
Apply definition of exp'
583 ALL(b):[x e n & b e n
=>
[~[x=0 & b=0] => exp'(x,b+1)=exp'(x,b)*x]]
U Spec, 469
584 x e n & y e n
=>
[~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x]
U Spec, 583
585 ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x
Detach, 584, 580
586 exp'(x,y+1)=exp'(x,y)*x
Detach, 585, 576
587 exp'(x,y+1)=exp(x,y)*x
Substitute, 577,
586
588 exp(x,y+1)=exp'(x,y+1)
Substitute, 587,
582
589 x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)
Arb Or, 588
590 y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)]
Join, 528, 589
591 y+1 e p
Detach, 534, 590
Case 2
As Required:
592 ~x=0 => y+1 e p
4 Conclusion, 571
593 [x=0 => y+1 e p] & [~x=0 => y+1 e p]
Join, 570, 592
594 y+1 e p
Cases, 471, 593
As Required:
595 ALL(b):[b e p => b+1 e p]
4 Conclusion, 514
596 0 e p & ALL(b):[b e p => b+1 e p]
Join, 513, 595
597 ALL(b):[b e n => b e p]
Detach, 486, 596
Prove: ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
Suppose...
598 y e n
Premise
599 y e n => y e p
U Spec, 597
600 y e p
Detach, 599, 598
Apply definition of p
601 y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
U Spec, 475
602 [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]
&
[y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]
Iff-And, 601
603 y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Split, 602
604 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p
Split, 602
605 y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
Detach, 603, 600
606 y e n
Split, 605
607 ~[x=0 & y=0] => exp(x,y)=exp'(x,y)
Split, 605
As Required:
608 ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
4 Conclusion, 598
As Required:
609 ALL(a):[a e n
=>
ALL(b):[b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]
4 Conclusion, 470
Prove: ALL(a):ALL(b):[a e n & b e n =>
[~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]
Suppose...
610 x e n & y e n
Premise
611 x e n
Split, 610
612 y e n
Split, 610
613 x e n
=>
ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
U Spec, 609
614 ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]
Detach, 613, 611
615 y e n => [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]
U Spec, 614
616 ~[x=0 & y=0] => exp(x,y)=exp'(x,y)
Detach, 615, 612
As Required:
617 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]
4 Conclusion, 610
As Required:
618 ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]
&
exp(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => 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) e n]]
&
exp'(0,1)=0
&
ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => 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, 460