THEOREM
*******
For all x0 e N, there exists a function
exp: NxN --> N such that, we
have:
1. exp(0,0) = x0
2. For all non-zero a, we have
exp(a,0)=1 (starting with exponent 0)
3. For all a, b e N, we have exp(a,b+1) = exp(a,b)*a
Where
exp(x,y) = x to the power of y
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-11-12
OUTLINE
*******
Lines Content
***** *******
1-13 Axioms/Definitions
14-36 Construct function exp: NxN --> N
starting with exponent 0
37-943 Prove functionality of exp
944-1063 Establish required
properties of the exp function
AXIOMS/DEFINITIONS
******************
Define: n, 0, 1, 2
******************
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
4 2 e n
Axiom
5 2=1+1
Axiom
Properties of +
***************
Closed on n
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Right cancelability of +
7 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]
Axiom
0 is not the successor of any
number
8 ALL(a):[a e n => ~a+1=0]
Axiom
Principle of mathematical
deduction using addition on n
9 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
10 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
11 ALL(a):[a e n => a*0=0]
Axiom
12 ALL(a):[a e n => a*1=a]
Axiom
13 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
CONSTRUCT exp FUNCTION
**********************
Suppose...
14 x0 e n
Premise
Construct n2
15 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
16 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, 15
17 Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 16
18 Set(n) & Set(n)
Join, 1, 1
19 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 17, 18
20 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 19
Define: n2
21 Set'(n2)
Split, 20
22 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 20
Construct n3
23 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
24 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, 23
25 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, 24
26 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, 25
27 Set(n) & Set(n)
Join, 1, 1
28 Set(n) & Set(n) & Set(n)
Join, 27, 1
29 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, 26, 28
30 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 29
Define: n3
31 Set''(n3)
Split, 30
32 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 30
Construct exp
33 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(a,b,c) e d]]]
Subset, 31
34 Set''(exp) & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(a,b,c) e d]]
E Spec, 33
Define: exp
35 Set''(exp)
Split, 34
36 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(a,b,c) e d]]
Split, 34
PROVE FUNCTIONALITIY OF exp
***************************
Apply Function Axiom
37 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
38 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, 37
39 ALL(cod):[Set''(exp) & Set'(n2) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e cod & (a1,a2,b) e exp]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & 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 n2 & b e cod => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]]]
U Spec, 38
40 Set''(exp) & Set'(n2) & Set(n)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e exp]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & 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 n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]]
U Spec, 39
41 Set''(exp) & Set'(n2)
Join, 35, 21
42 Set''(exp) & Set'(n2) & Set(n)
Join, 41, 1
Sufficient: For functionality of exp
43 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e exp]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & 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 n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]
Detach, 40, 42
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => a e n & b e n & c e n]
Suppose...
44 (x,y,z) e exp
Premise
45 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,b,c) e d]]
U Spec, 36
46 ALL(c):[(x,y,c) e exp
<=>
(x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,c) e d]]
U Spec, 45
47 (x,y,z) e exp
<=>
(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
U Spec, 46
48 [(x,y,z) e exp => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d] => (x,y,z) e exp]
Iff-And, 47
49 (x,y,z) e exp => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Split, 48
50 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d] => (x,y,z) e exp
Split, 48
51 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Detach, 49, 44
52 (x,y,z) e n3
Split, 51
53 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Split, 51
54 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 32
55 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 54
56 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 55
57 [(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, 56
58 (x,y,z) e n3 => x e n & y e n & z e n
Split, 57
59 x e n & y e n & z e n => (x,y,z) e n3
Split, 57
60 x e n & y e n & z e n
Detach, 58, 52
As Required:
61 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => a e n & b e n & c e n]
4 Conclusion, 44
62 ALL(b):ALL(c):[(0,b,c) e exp
<=>
(0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,b,c) e d]]
U Spec, 36
63 ALL(c):[(0,0,c) e exp
<=>
(0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,c) e d]]
U Spec, 62
64 (0,0,x0) e exp
<=>
(0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d]
U Spec, 63
65 [(0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d]]
&
[(0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d] => (0,0,x0) e exp]
Iff-And, 64
66 (0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d]
Split, 65
Sufficient: For (0,0,x0) e exp
67 (0,0,x0) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d] => (0,0,x0) e exp
Split, 65
68 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 32
69 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 68
70 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 69
71 [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]
&
[0 e n & 0 e n & x0 e n => (0,0,x0) e n3]
Iff-And, 70
72 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 71
73 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 71
74 0 e n & 0 e n
Join, 2, 2
75 0 e n & 0 e n & x0 e n
Join, 74, 14
76 (0,0,x0) e n3
Detach, 73, 75
77 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Premise
78 Set''(d)
Split, 77
79 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 77
80 (0,0,x0) e d
Split, 77
81 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d]
4 Conclusion, 77
82 (0,0,x0) e n3
&
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,x0) e d]
Join, 76, 81
As Required:
83 (0,0,x0) e exp
Detach, 67, 82
Prove: ALL(a):[a e n => [~a=0
=> (a,0,1) e exp]]
Suppose...
84 x e n
Premise
Prove: ~x=0 => (x,0,1) e exp
Suppose...
85 ~x=0
Premise
86 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,b,c) e d]]
U Spec, 36
87 ALL(c):[(x,0,c) e exp
<=>
(x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,c) e d]]
U Spec, 86
88 (x,0,1) e exp
<=>
(x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d]
U Spec, 87
89 [(x,0,1) e exp => (x,0,1) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d]]
&
[(x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d] => (x,0,1) e exp]
Iff-And, 88
90 (x,0,1) e exp => (x,0,1) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d]
Split, 89
Sufficient: For (x,0,1) e exp
91 (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d] => (x,0,1) e exp
Split, 89
92 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 32
93 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 92
94 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n
U Spec, 93
95 [(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, 94
96 (x,0,1) e n3 => x e n & 0 e n & 1 e n
Split, 95
97 x e n & 0 e n & 1 e n => (x,0,1) e n3
Split, 95
98 x e n & 0 e n
Join, 84, 2
99 x e n & 0 e n & 1 e n
Join, 98, 3
100 (x,0,1) e n3
Detach, 97, 99
101 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Premise
102 Set''(d)
Split, 101
103 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 101
104 (0,0,x0) e d
Split, 101
105 ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
Split, 101
106 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Split, 101
107 x e n => [~x=0 => (x,0,1) e d]
U Spec, 105
108 ~x=0 => (x,0,1) e d
Detach, 107, 84
109 (x,0,1) e d
Detach, 108, 85
110 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d]
4 Conclusion, 101
111 (x,0,1) e n3
&
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,1) e d]
Join, 100, 110
112 (x,0,1) e exp
Detach, 91, 111
As Required:
113 ~x=0 => (x,0,1) e exp
4 Conclusion, 85
As Required:
114 ALL(a):[a e n => [~a=0 => (a,0,1) e exp]]
4 Conclusion, 84
Suppose...
115 x e n & y e n & z e n
Premise
116 x e n
Split, 115
117 y e n
Split, 115
118 z e n
Split, 115
Suppose...
119 (x,y,z) e exp
Premise
120 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,b,c) e d]]
U Spec, 36
121 ALL(c):[(x,y,c) e exp
<=>
(x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,c) e d]]
U Spec, 120
122 (x,y,z) e exp
<=>
(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
U Spec, 121
123 [(x,y,z) e exp => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d] => (x,y,z) e exp]
Iff-And, 122
124 (x,y,z) e exp => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Split, 123
125 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d] => (x,y,z) e exp
Split, 123
126 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Detach, 124, 119
127 (x,y,z) e n3
Split, 126
128 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d]
Split, 126
129 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
130 y e n & 1 e n => y+1 e n
U Spec, 129
131 y e n & 1 e n
Join, 117, 3
132 y+1 e n
Detach, 130, 131
133 ALL(b):[z e n & b e n => z*b e n]
U Spec, 10
134 z e n & x e n => z*x e n
U Spec, 133
135 z e n & x e n
Join, 118, 116
136 z*x e n
Detach, 134, 135
137 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,b,c) e d]]
U Spec, 36
138 ALL(c):[(x,y+1,c) e exp
<=>
(x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,c) e d]]
U Spec, 137, 132
139 (x,y+1,z*x) e exp
<=>
(x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d]
U Spec, 138, 136
140 [(x,y+1,z*x) e exp => (x,y+1,z*x) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d]]
&
[(x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d] => (x,y+1,z*x) e exp]
Iff-And, 139
141 (x,y+1,z*x) e exp => (x,y+1,z*x) e n3 & ALL(d):[Set''(d)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d]
Split, 140
Sufficient: For (x,y+1,z*x) e exp
142 (x,y+1,z*x) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d] => (x,y+1,z*x) e exp
Split, 140
143 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 32
144 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]
U Spec, 143, 132
145 (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n
U Spec, 144, 136
146 [(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, 145
147 (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n
Split, 146
148 x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3
Split, 146
149 x e n & y+1 e n
Join, 116, 132
150 x e n & y+1 e n & z*x e n
Join, 149, 136
151 (x,y+1,z*x) e n3
Detach, 148, 150
152 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Premise
153 Set''(d)
Split, 152
154 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 152
155 (0,0,x0) e d
Split, 152
156 ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
Split, 152
157 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Split, 152
158 ALL(f):ALL(g):[(x,f,g) e d => (x,f+1,g*x) e d]
U Spec, 157
159 ALL(g):[(x,y,g) e d => (x,y+1,g*x) e d]
U Spec, 158
160 (x,y,z) e d => (x,y+1,z*x) e d
U Spec, 159
161 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y,z) e d
U Spec, 128
162 (x,y,z) e d
Detach, 161, 152
163 (x,y+1,z*x) e d
Detach, 160, 162
164 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d]
4 Conclusion, 152
165 (x,y+1,z*x) e n3
&
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z*x) e d]
Join, 151, 164
166 (x,y+1,z*x) e exp
Detach, 142, 165
167 (x,y,z) e exp => (x,y+1,z*x) e exp
4 Conclusion, 119
As Required:
168 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=>
[(a,b,c) e exp => (a,b+1,c*a) e exp]]
4 Conclusion, 115
Prove: ALL(c):[c e n =>
[(0,0,c) e exp => c=x0]]
Suppose...
169 z e n
Premise
Prove: ~~[(0,0,z) e exp =>
z=x0]
Suppose to the contrary...
170 ~[(0,0,z) e exp => z=x0]
Premise
171 ~~[(0,0,z) e exp & ~z=x0]
Imply-And, 170
172 (0,0,z) e exp & ~z=x0
Rem DNeg, 171
173 (0,0,z) e exp
Split, 172
174 ~z=x0
Split, 172
175 ALL(b):ALL(c):[(0,b,c) e exp
<=>
(0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,b,c) e d]]
U Spec, 36
176 ALL(c):[(0,0,c) e exp
<=>
(0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,c) e d]]
U Spec, 175
177 (0,0,z) e exp
<=>
(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d]
U Spec, 176
178 [(0,0,z) e exp => (0,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d]]
&
[(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d] => (0,0,z) e exp]
Iff-And, 177
179 (0,0,z) e exp => (0,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d]
Split, 178
180 (0,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d] => (0,0,z) e exp
Split, 178
181 ~[(0,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d]] => ~(0,0,z) e exp
Contra, 179
182 ~~[~(0,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d]] => ~(0,0,z) e exp
DeMorgan, 181
183 ~(0,0,z) e n3 | ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d] => ~(0,0,z) e exp
Rem DNeg, 182
184 ~(0,0,z) e n3 | ~~EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d] => ~(0,0,z) e exp
Quant, 183
185 ~(0,0,z) e n3 | EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(0,0,z) e d] => ~(0,0,z) e exp
Rem DNeg, 184
186 ~(0,0,z) e n3 | EXIST(d):~~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e exp
Imply-And, 185
Sufficient: For ~(0,0,z) e exp (to obtain a contradiction)
187 ~(0,0,z) e n3 | EXIST(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e exp
Rem DNeg, 186
Construct q
188 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e exp & ~[a=0 & b=0 & c=z]]]
Subset, 35
189 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e exp & ~[a=0 & b=0 & c=z]]
E Spec, 188
Define: q
190 Set''(q)
Split, 189
191 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e exp & ~[a=0 & b=0 & c=z]]
Split, 189
Prove: ALL(d):ALL(e):ALL(f):[(d,e,f) e q => d e n & e e n & f e n]
Suppose...
192 (t,u,v) e q
Premise
193 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=0 & b=0 & c=z]]
U Spec, 191
194 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e exp & ~[t=0 & u=0 & c=z]]
U Spec, 193
195 (t,u,v) e q
<=>
(t,u,v) e exp & ~[t=0 & u=0 & v=z]
U Spec, 194
196 [(t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]]
&
[(t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q]
Iff-And, 195
197 (t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]
Split, 196
198 (t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 196
199 (t,u,v) e exp & ~[t=0 & u=0 & v=z]
Detach, 197, 192
200 (t,u,v) e exp
Split, 199
201 ~[t=0 & u=0 & v=z]
Split, 199
202 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]
U Spec, 61
203 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]
U Spec, 202
204 (t,u,v) e exp => t e n & u e n & v e n
U Spec, 203
205 t e n & u e n & v e n
Detach, 204, 200
As Required:
206 ALL(d):ALL(e):ALL(f):[(d,e,f) e q => d e n & e e n & f e n]
4 Conclusion, 192
As Required:
207 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
Rename, 206
208 ALL(b):ALL(c):[(0,b,c) e q
<=>
(0,b,c) e exp & ~[0=0 & b=0 & c=z]]
U Spec, 191
209 ALL(c):[(0,0,c) e q
<=>
(0,0,c) e exp & ~[0=0 & 0=0 & c=z]]
U Spec, 208
210 (0,0,x0) e q
<=>
(0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]
U Spec, 209
211 [(0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]]
&
[(0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q]
Iff-And, 210
212 (0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]
Split, 211
213 (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q
Split, 211
214 0=0 & 0=0 & x0=z
Premise
215 0=0
Split, 214
216 0=0
Split, 214
217 x0=z
Split, 214
218 z=x0
Sym, 217
219 z=x0 & ~z=x0
Join, 218, 174
220 ~[0=0 & 0=0 & x0=z]
4 Conclusion, 214
221 (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]
Join, 83, 220
As Required:
222 (0,0,x0) e q
Detach, 213, 221
Prove: ALL(e):[e e n => [~e=0
=> (e,0,1) e q]]
Suppose...
223 x e n
Premise
Prove: ~x=0 => (x,0,1) e q
Suppose...
224 ~x=0
Premise
225 ALL(b):ALL(c):[(x,b,c) e q
<=>
(x,b,c) e exp & ~[x=0 & b=0 & c=z]]
U Spec, 191
226 ALL(c):[(x,0,c) e q
<=>
(x,0,c) e exp & ~[x=0 & 0=0 & c=z]]
U Spec, 225
227 (x,0,1) e q
<=>
(x,0,1) e exp & ~[x=0 & 0=0 & 1=z]
U Spec, 226
228 [(x,0,1) e q => (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]]
&
[(x,0,1) e exp & ~[x=0 & 0=0 & 1=z] => (x,0,1) e q]
Iff-And, 227
229 (x,0,1) e q => (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]
Split, 228
230 (x,0,1) e exp & ~[x=0 & 0=0 & 1=z] => (x,0,1) e q
Split, 228
231 x e n => [~x=0 => (x,0,1) e exp]
U Spec, 114
232 ~x=0 => (x,0,1) e exp
Detach, 231, 223
233 (x,0,1) e exp
Detach, 232, 224
234 x=0 & 0=0 & 1=z
Premise
235 x=0
Split, 234
236 0=0
Split, 234
237 1=z
Split, 234
238 x=0 & ~x=0
Join, 235, 224
239 ~[x=0 & 0=0 & 1=z]
4 Conclusion, 234
240 (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]
Join, 233, 239
241 (x,0,1) e q
Detach, 230, 240
As Required:
242 ~x=0 => (x,0,1) e q
4 Conclusion, 224
As Required:
243 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 223
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Suppose...
244 (t,u,v) e q
Premise
245 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=0 & b=0 & c=z]]
U Spec, 191
246 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e exp & ~[t=0 & u=0 & c=z]]
U Spec, 245
247 (t,u,v) e q
<=>
(t,u,v) e exp & ~[t=0 & u=0 & v=z]
U Spec, 246
248 [(t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]]
&
[(t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q]
Iff-And, 247
249 (t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]
Split, 248
250 (t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 248
251 (t,u,v) e exp & ~[t=0 & u=0 & v=z]
Detach, 249, 244
252 (t,u,v) e exp
Split, 251
253 ~[t=0 & u=0 & v=z]
Split, 251
254 ALL(b):ALL(c):[(t,b,c) e exp
<=>
(t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,b,c) e d]]
U Spec, 36
255 ALL(c):[(t,u,c) e exp
<=>
(t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,c) e d]]
U Spec, 254
256 (t,u,v) e exp
<=>
(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
U Spec, 255
257 [(t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp]
Iff-And, 256
258 (t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 257
259 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp
Split, 257
260 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Detach, 258, 252
261 (t,u,v) e n3
Split, 260
262 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 260
263 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 32
264 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 263
265 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 264
266 [(t,u,v) e n3 => t e n & u e n & v e n]
&
[t e n & u e n & v e n => (t,u,v) e n3]
Iff-And, 265
267 (t,u,v) e n3 => t e n & u e n & v e n
Split, 266
268 t e n & u e n & v e n => (t,u,v) e n3
Split, 266
269 t e n & u e n & v e n
Detach, 267, 261
270 t e n
Split, 269
271 u e n
Split, 269
272 v e n
Split, 269
273 ALL(b):[u e n & b e n => u+b e n]
U Spec, 6
274 u e n & 1 e n => u+1 e n
U Spec, 273
275 u e n & 1 e n
Join, 271, 3
276 u+1 e n
Detach, 274, 275
277 ALL(b):[v e n & b e n => v*b e n]
U Spec, 10
278 v e n & t e n => v*t e n
U Spec, 277
279 v e n & t e n
Join, 272, 270
280 v*t e n
Detach, 278, 279
281 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=0 & b=0 & c=z]]
U Spec, 191
282 ALL(c):[(t,u+1,c) e q
<=>
(t,u+1,c) e exp & ~[t=0 & u+1=0 & c=z]]
U Spec, 281, 276
283 (t,u+1,v*t) e q
<=>
(t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]
U Spec, 282, 280
284 [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]]
&
[(t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q]
Iff-And, 283
285 (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]
Split, 284
Sufficient: For (t,u+1,v*t) e q
286 (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q
Split, 284
287 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e exp => (t,b+1,c*t) e exp]]
U Spec, 168
288 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e exp => (t,u+1,c*t) e exp]]
U Spec, 287
289 t e n & u e n & v e n
=>
[(t,u,v) e exp => (t,u+1,v*t) e exp]
U Spec, 288
290 (t,u,v) e exp => (t,u+1,v*t) e exp
Detach, 289, 269
291 (t,u+1,v*t) e exp
Detach, 290, 252
Prove: ~[t=0 & u+1=0 & v*t=z]
Suppose to the contrary...
292 t=0 & u+1=0 & v*t=z
Premise
293 t=0
Split, 292
294 u+1=0
Split, 292
295 v*t=z
Split, 292
296 u e n => ~u+1=0
U Spec, 8
297 ~u+1=0
Detach, 296, 271
298 u+1=0 & ~u+1=0
Join, 294, 297
As Required:
299 ~[t=0 & u+1=0 & v*t=z]
4 Conclusion, 292
300 (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]
Join, 291, 299
301 (t,u+1,v*t) e q
Detach, 286, 300
As Required:
302 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 244
303 ALL(b):ALL(c):[(0,b,c) e q
<=>
(0,b,c) e exp & ~[0=0 & b=0 & c=z]]
U Spec, 191
304 ALL(c):[(0,0,c) e q
<=>
(0,0,c) e exp & ~[0=0 & 0=0 & c=z]]
U Spec, 303
305 (0,0,z) e q
<=>
(0,0,z) e exp & ~[0=0 & 0=0 & z=z]
U Spec, 304
306 [(0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]]
&
[(0,0,z) e exp & ~[0=0 & 0=0 & z=z] => (0,0,z) e q]
Iff-And, 305
307 (0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]
Split, 306
308 (0,0,z) e exp & ~[0=0 & 0=0 & z=z] => (0,0,z) e q
Split, 306
309 ~[(0,0,z) e exp & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
Contra, 307
310 ~~[~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
DeMorgan, 309
311 ~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q
Rem DNeg, 310
312 ~(0,0,z) e exp | 0=0 & 0=0 & z=z => ~(0,0,z) e q
Rem DNeg, 311
313 0=0
Reflex
314 z=z
Reflex
315 0=0 & 0=0
Join, 313, 313
316 0=0 & 0=0 & z=z
Join, 315, 314
317 ~(0,0,z) e exp | 0=0 & 0=0 & z=z
Arb Or, 316
As Required:
318 ~(0,0,z) e q
Detach, 312, 317
319 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
Join, 190, 207
320 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
Join, 319, 222
321 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 320, 243
322 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Join, 321, 302
323 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
&
~(0,0,z) e q
Join, 322, 318
324 EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(0,0,z) e d]
E Gen, 323
325 ~(0,0,z) e n3 | EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(0,0,z) e d]
Arb Or, 324
326 ~(0,0,z) e exp
Detach, 187, 325
327 (0,0,z) e exp & ~(0,0,z) e exp
Join, 173, 326
As Required:
328 ~~[(0,0,z) e exp => z=x0]
4 Conclusion, 170
329 (0,0,z) e exp => z=x0
Rem DNeg, 328
As Required:
330 ALL(c):[c e n => [(0,0,c) e exp => c=x0]]
4 Conclusion, 169
Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
Suppose...
331 (x,y,z) e exp
Premise
332 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n]
U Spec, 61
333 ALL(c):[(x,y,c) e exp => x e n & y e n & c e n]
U Spec, 332
334 (x,y,z) e exp => x e n & y e n & z e n
U Spec, 333
335 x e n & y e n & z e n
Detach, 334, 331
336 x e n
Split, 335
337 y e n
Split, 335
338 z e n
Split, 335
339 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
340 (x,y) e n2 <=> x e n & y e n
U Spec, 339
341 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 340
342 (x,y) e n2 => x e n & y e n
Split, 341
343 x e n & y e n => (x,y) e n2
Split, 341
344 x e n & y e n
Join, 336, 337
345 (x,y) e n2
Detach, 343, 344
346 (x,y) e n2 & z e n
Join, 345, 338
Functionality, Part 1
347 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
4 Conclusion, 331
Prove: ALL(a):[a e n
=> ALL(b):[b
e n => EXIST(c):[c e n &
(a,b,c) e exp]]]
Suppose...
348 x e n
Premise
349 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]]
Subset, 1
350 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]
E Spec, 349
Define: p1
351 Set(p1)
Split, 350
352 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]
Split, 350
353 Set(p1) & ALL(b):[b e p1 => b e n]
=>
[0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=>
ALL(b):[b e n => b e p1]]
U Spec, 9
354 t e p1
Premise
355 t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e exp]
U Spec, 352
356 [t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e exp]]
&
[t e n & EXIST(c):[c e n & (x,t,c) e exp] => t e p1]
Iff-And, 355
357 t e p1 => t e n &
EXIST(c):[c e n & (x,t,c) e exp]
Split, 356
358 t e n & EXIST(c):[c e n & (x,t,c) e exp] => t e p1
Split, 356
359 t e n & EXIST(c):[c e n & (x,t,c) e exp]
Detach, 357, 354
360 t e n
Split, 359
361 ALL(b):[b e p1 => b e n]
4 Conclusion, 354
362 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 351, 361
Sufficient: For ALL(b):[b e n => b e p1]
363 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=>
ALL(b):[b e n => b e p1]
Detach, 353, 362
364 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e exp]
U Spec, 352
365 [0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e exp]]
&
[0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p1]
Iff-And, 364
366 0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e exp]
Split, 365
367 0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p1
Split, 365
368 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e exp]
U Spec, 352
369 [0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e exp]]
&
[0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p1]
Iff-And, 368
370 0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e exp]
Split, 369
Sufficient: For 0 e p1
371 0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p1
Split, 369
Two cases to consider:
372 x=0 | ~x=0
Or Not
Case 1
373 x=0
Premise
374 (x,0,x0) e exp
Substitute, 373,
83
375 x0 e n & (x,0,x0) e exp
Join, 14, 374
376 EXIST(c):[c e n & (x,0,c) e exp]
E Gen, 375
As Required:
377 x=0 => EXIST(c):[c e n & (x,0,c) e exp]
4 Conclusion, 373
Case 2
Prove: ~x=0 => EXIST(c):[c e n & (x,0,c) e exp]
Suppose...
378 ~x=0
Premise
379 x e n => [~x=0 => (x,0,1) e exp]
U Spec, 114
380 ~x=0 => (x,0,1) e exp
Detach, 379, 348
381 (x,0,1) e exp
Detach, 380, 378
382 1 e n & (x,0,1) e exp
Join, 3, 381
383 EXIST(c):[c e n & (x,0,c) e exp]
E Gen, 382
As Required:
384 ~x=0 => EXIST(c):[c e n & (x,0,c) e exp]
4 Conclusion, 378
385 [x=0 => EXIST(c):[c e n & (x,0,c) e exp]]
&
[~x=0 =>
EXIST(c):[c e n & (x,0,c) e exp]]
Join, 377, 384
386 EXIST(c):[c e n & (x,0,c) e exp]
Cases, 372, 385
387 0 e n & EXIST(c):[c e n & (x,0,c) e exp]
Join, 2, 386
As Required:
388 0 e p1
Detach, 371, 387
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
389 y e p1
Premise
390 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 352
391 [y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e exp]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p1]
Iff-And, 390
392 y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e exp]
Split, 391
393 y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p1
Split, 391
394 y e n & EXIST(c):[c e n & (x,y,c) e exp]
Detach, 392, 389
395 y e n
Split, 394
396 EXIST(c):[c e n & (x,y,c) e exp]
Split, 394
397 z e n & (x,y,z) e exp
E Spec, 396
398 z e n
Split, 397
399 (x,y,z) e exp
Split, 397
400 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
401 y e n & 1 e n => y+1 e n
U Spec, 400
402 y e n & 1 e n
Join, 395, 3
403 y+1 e n
Detach, 401, 402
404 ALL(b):[z e n & b e n => z*b e n]
U Spec, 10
405 z e n & x e n => z*x e n
U Spec, 404
406 z e n & x e n
Join, 398, 348
407 z*x e n
Detach, 405, 406
408 y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]
U Spec, 352, 403
409 [y+1 e p1 => y+1 e n &
EXIST(c):[c e n & (x,y+1,c) e exp]]
&
[y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp] => y+1 e p1]
Iff-And, 408
410 y+1 e p1 => y+1 e n &
EXIST(c):[c e n & (x,y+1,c) e exp]
Split, 409
Sufficient:
411 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp] => y+1 e p1
Split, 409
412 ALL(b):ALL(c):[x e n & b e n & c e n
=>
[(x,b,c) e exp => (x,b+1,c*x) e exp]]
U Spec, 168
413 ALL(c):[x e n & y e n & c e n
=>
[(x,y,c) e exp => (x,y+1,c*x) e exp]]
U Spec, 412
414 x e n & y e n & z e n
=>
[(x,y,z) e exp => (x,y+1,z*x) e exp]
U Spec, 413
415 x e n & y e n
Join, 348, 395
416 x e n & y e n & z e n
Join, 415, 398
417 (x,y,z) e exp => (x,y+1,z*x) e exp
Detach, 414, 416
418 (x,y+1,z*x) e exp
Detach, 417, 399
419 z*x e n & (x,y+1,z*x) e exp
Join, 407, 418
420 EXIST(c):[c e n & (x,y+1,c) e exp]
E Gen, 419
421 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]
Join, 403, 420
422 y+1 e p1
Detach, 411, 421
As Required:
423 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 389
424 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 388, 423
425 ALL(b):[b e n => b e p1]
Detach, 363, 424
Prove: ALL(b):[b e n =>
EXIST(c):[c e n & (x,b,c) e exp]]
Suppose...
426 y e n
Premise
427 y e n => y e p1
U Spec, 425
428 y e p1
Detach, 427, 426
429 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 352
430 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e exp]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p1]
Iff-And, 429
431 y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e exp]
Split, 430
432 y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p1
Split, 430
433 y e n & EXIST(c):[c e n & (x,y,c) e exp]
Detach, 431, 428
434 y e n
Split, 433
435 EXIST(c):[c e n & (x,y,c) e exp]
Split, 433
As Required:
436 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]
4 Conclusion, 426
As Required:
437 ALL(a):[a e n
=>
ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e exp]]]
4 Conclusion, 348
Prove: ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n &
(a1,a2,c) e exp]]
Suppose...
438 (x,y) e n2
Premise
439 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
440 (x,y) e n2 <=> x e n & y e n
U Spec, 439
441 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 440
442 (x,y) e n2 => x e n & y e n
Split, 441
443 x e n & y e n => (x,y) e n2
Split, 441
444 x e n & y e n
Detach, 442, 438
445 x e n
Split, 444
446 y e n
Split, 444
447 x e n
=>
ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]
U Spec, 437
448 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]
Detach, 447, 445
449 y e n => EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 448
450 EXIST(c):[c e n & (x,y,c) e exp]
Detach, 449, 446
Functionality, Part 2
451 ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]
4 Conclusion, 438
Prove: ALL(a):[a e n
=> ALL(b):[b
e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e exp &
(a,b,c2) e exp => c1=c2]]]]
Suppose...
452 x e n
Premise
453 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]]
Subset, 1
454 Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]
E Spec, 453
Define: p2
455 Set(p2)
Split, 454
456 ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]
Split, 454
457 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, 9
458 0 e p2 <=> 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]]
U Spec, 456
459 [0 e p2 => 0 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]]]
&
[0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]] => 0 e p2]
Iff-And, 458
460 0 e p2 => 0 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]]
Split, 459
Sufficient:
461 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]] => 0 e p2
Split, 459
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,0,c1) e exp & (x,0,c2) e exp =>
c1=c2]]
Suppose...
462 z1 e n & z2 e n
Premise
463 z1 e n
Split, 462
464 z2 e n
Split, 462
Prove: (x,0,z1) e exp &
(x,0,z2) e exp => z1=z2
Suppose...
465 (x,0,z1) e exp & (x,0,z2) e exp
Premise
466 (x,0,z1) e exp
Split, 465
467 (x,0,z2) e exp
Split, 465
Two cases:
468 x=0 | ~x=0
Or Not
Case 1
Prove: x=0 => z1=z2
Suppose...
469 x=0
Premise
470 (0,0,z1) e exp
Substitute, 469,
466
471 (0,0,z2) e exp
Substitute, 469,
467
472 z1 e n => [(0,0,z1) e exp => z1=x0]
U Spec, 330
473 (0,0,z1) e exp => z1=x0
Detach, 472, 463
474 z1=x0
Detach, 473, 470
475 z2 e n => [(0,0,z2) e exp => z2=x0]
U Spec, 330
476 (0,0,z2) e exp => z2=x0
Detach, 475, 464
477 z2=x0
Detach, 476, 471
478 z1=z2
Substitute, 477,
474
As Required:
479 x=0 => z1=z2
4 Conclusion, 469
Case 2
Prove: ~x=0 => z1=z2
Suppose...
480 ~x=0
Premise
Prove: ALL(c):[c e n => [(x,0,c) e exp =>
c=1]]
Suppose...
481 z e n
Premise
Suppose...
482 ~[(x,0,z) e exp => z=1]
Premise
483 ~~[(x,0,z) e exp & ~z=1]
Imply-And, 482
484 (x,0,z) e exp & ~z=1
Rem DNeg, 483
485 (x,0,z) e exp
Split, 484
486 ~z=1
Split, 484
487 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
488 ALL(c):[(x,0,c) e exp
<=>
(x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,c) e d]]
U Spec, 487
489 (x,0,z) e exp
<=>
(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d]
U Spec, 488
490 [(x,0,z) e exp => (x,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d]]
&
[(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d] => (x,0,z) e exp]
Iff-And, 489
491 (x,0,z) e exp => (x,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d]
Split, 490
492 (x,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d] => (x,0,z) e exp
Split, 490
493 ~[(x,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d]] => ~(x,0,z) e exp
Contra, 491
494 ~~[~(x,0,z) e n3 | ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d]] => ~(x,0,z) e exp
DeMorgan, 493
495 ~(x,0,z) e n3 | ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d] => ~(x,0,z) e exp
Rem DNeg, 494
496 ~(x,0,z) e n3 | ~~EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d] => ~(x,0,z) e exp
Quant, 495
497 ~(x,0,z) e n3 | EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,0,z) e d] => ~(x,0,z) e exp
Rem DNeg, 496
498 ~(x,0,z) e n3 | EXIST(d):~~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& (0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e exp
Imply-And, 497
499 ~(x,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e exp
Rem DNeg, 498
500 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e exp & ~[a=x & b=0 & c=z]]]
Subset, 35
501 Set''(q2) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=>
(a,b,c) e exp & ~[a=x & b=0 & c=z]]
E Spec, 500
Define: q2
502 Set''(q2)
Split, 501
503 ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=>
(a,b,c) e exp & ~[a=x & b=0 & c=z]]
Split, 501
Suppose...
504 (t,u,v) e q2
Premise
505 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e exp & ~[t=x & b=0 & c=z]]
U Spec, 503
506 ALL(c):[(t,u,c) e q2
<=>
(t,u,c) e exp & ~[t=x & u=0 & c=z]]
U Spec, 505
507 (t,u,v) e q2
<=> (t,u,v) e exp & ~[t=x & u=0 & v=z]
U Spec, 506
508 [(t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2]
Iff-And, 507
509 (t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]
Split, 508
510 (t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2
Split, 508
511 (t,u,v) e exp & ~[t=x & u=0 & v=z]
Detach, 509, 504
512 (t,u,v) e exp
Split, 511
513 ~[t=x & u=0 & v=z]
Split, 511
514 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]
U Spec, 61
515 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]
U Spec, 514
516 (t,u,v) e exp => t e n & u e n & v e n
U Spec, 515
517 t e n & u e n & v e n
Detach, 516, 512
As Required:
518 ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
4 Conclusion, 504
519 ALL(b):ALL(c):[(0,b,c) e q2
<=> (0,b,c) e exp & ~[0=x & b=0 & c=z]]
U Spec, 503
520 ALL(c):[(0,0,c) e q2
<=>
(0,0,c) e exp & ~[0=x & 0=0 & c=z]]
U Spec, 519
521 (0,0,x0) e q2
<=>
(0,0,x0) e exp & ~[0=x & 0=0 & x0=z]
U Spec, 520
522 [(0,0,x0) e q2 => (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]]
&
[(0,0,x0) e exp & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q2]
Iff-And, 521
523 (0,0,x0) e q2 => (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]
Split, 522
Sufficient:
524 (0,0,x0) e exp & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q2
Split, 522
525 0=x & 0=0 & x0=z
Premise
526 0=x
Split, 525
527 0=0
Split, 525
528 x0=z
Split, 525
529 x=0
Sym, 526
530 x=0 & ~x=0
Join, 529, 480
531 ~[0=x & 0=0 & x0=z]
4 Conclusion, 525
532 (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]
Join, 83, 531
As Required:
533 (0,0,x0) e q2
Detach, 524, 532
534 t e n
Premise
535 ~t=0
Premise
536 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e exp & ~[t=x & b=0 & c=z]]
U Spec, 503
537 ALL(c):[(t,0,c) e q2
<=>
(t,0,c) e exp & ~[t=x & 0=0 & c=z]]
U Spec, 536
538 (t,0,1) e q2
<=>
(t,0,1) e exp & ~[t=x & 0=0 & 1=z]
U Spec, 537
539 [(t,0,1) e q2 => (t,0,1) e exp & ~[t=x & 0=0 & 1=z]]
&
[(t,0,1) e exp & ~[t=x & 0=0 & 1=z] => (t,0,1) e q2]
Iff-And, 538
540 (t,0,1) e q2 => (t,0,1) e exp & ~[t=x & 0=0 & 1=z]
Split, 539
Sufficient:
541 (t,0,1) e exp & ~[t=x & 0=0 & 1=z] => (t,0,1) e q2
Split, 539
542 t e n => [~t=0 => (t,0,1) e exp]
U Spec, 114
543 ~t=0 => (t,0,1) e exp
Detach, 542, 534
544 (t,0,1) e exp
Detach, 543, 535
545 t=x & 0=0 & 1=z
Premise
546 t=x
Split, 545
547 0=0
Split, 545
548 1=z
Split, 545
549 z=1
Sym, 548
550 z=1 & ~z=1
Join, 549, 486
551 ~[t=x & 0=0 & 1=z]
4 Conclusion, 545
552 (t,0,1) e exp & ~[t=x & 0=0 & 1=z]
Join, 544, 551
553 (t,0,1) e q2
Detach, 541, 552
554 ~t=0 => (t,0,1) e q2
4 Conclusion, 535
As Required:
555 ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]
4 Conclusion, 534
Suppose...
556 (t,u,v) e q2
Premise
557 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e exp & ~[t=x & b=0 & c=z]]
U Spec, 503
558 ALL(c):[(t,u,c) e q2
<=>
(t,u,c) e exp & ~[t=x & u=0 & c=z]]
U Spec, 557
559 (t,u,v) e q2
<=>
(t,u,v) e exp & ~[t=x & u=0 & v=z]
U Spec, 558
560 [(t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2]
Iff-And, 559
561 (t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]
Split, 560
562 (t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2
Split, 560
563 (t,u,v) e exp & ~[t=x & u=0 & v=z]
Detach, 561, 556
564 (t,u,v) e exp
Split, 563
565 ~[t=x & u=0 & v=z]
Split, 563
566 ALL(b):ALL(c):[(t,b,c) e exp
<=>
(t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,b,c) e d]]
U Spec, 36
567 ALL(c):[(t,u,c) e exp
<=>
(t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,c) e d]]
U Spec, 566
568 (t,u,v) e exp
<=>
(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
U Spec, 567
569 [(t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& (0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp]
Iff-And, 568
570 (t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 569
571 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp
Split, 569
572 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Detach, 570, 564
573 (t,u,v) e n3
Split, 572
574 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& (0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 572
575 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]
U Spec, 61
576 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]
U Spec, 575
577 (t,u,v) e exp => t e n & u e n & v e n
U Spec, 576
578 t e n & u e n & v e n
Detach, 577, 564
579 t e n
Split, 578
580 u e n
Split, 578
581 v e n
Split, 578
582 ALL(b):[u e n & b e n => u+b e n]
U Spec, 6
583 u e n & 1 e n => u+1 e n
U Spec, 582
584 u e n & 1 e n
Join, 580, 3
585 u+1 e n
Detach, 583, 584
586 ALL(b):[v e n & b e n => v*b e n]
U Spec, 10
587 v e n & t e n => v*t e n
U Spec, 586
588 v e n & t e n
Join, 581, 579
589 v*t e n
Detach, 587, 588
590 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e exp & ~[t=x & b=0 & c=z]]
U Spec, 503
591 ALL(c):[(t,u+1,c) e q2
<=>
(t,u+1,c) e exp & ~[t=x & u+1=0 & c=z]]
U Spec, 590, 585
592 (t,u+1,v*t) e q2
<=>
(t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]
U Spec, 591, 589
593 [(t,u+1,v*t) e q2 => (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]]
&
[(t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q2]
Iff-And, 592
594 (t,u+1,v*t) e q2 => (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]
Split, 593
Sufficient:
595 (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q2
Split, 593
596 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e exp => (t,b+1,c*t) e exp]]
U Spec, 168
597 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e exp => (t,u+1,c*t) e exp]]
U Spec, 596
598 t e n & u e n & v e n
=>
[(t,u,v) e exp => (t,u+1,v*t) e exp]
U Spec, 597
599 (t,u,v) e exp => (t,u+1,v*t) e exp
Detach, 598, 578
600 (t,u+1,v*t) e exp
Detach, 599, 564
601 t=x & u+1=0 & v*t=z
Premise
602 t=x
Split, 601
603 u+1=0
Split, 601
604 v*t=z
Split, 601
605 u e n => ~u+1=0
U Spec, 8
606 ~u+1=0
Detach, 605, 580
607 u+1=0 & ~u+1=0
Join, 603, 606
608 ~[t=x & u+1=0 & v*t=z]
4 Conclusion, 601
609 (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]
Join, 600, 608
610 (t,u+1,v*t) e q2
Detach, 595, 609
As Required:
611 ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]
4 Conclusion, 556
612 ALL(b):ALL(c):[(x,b,c) e q2
<=>
(x,b,c) e exp & ~[x=x & b=0 & c=z]]
U Spec, 503
613 ALL(c):[(x,0,c) e q2
<=>
(x,0,c) e exp & ~[x=x & 0=0 & c=z]]
U Spec, 612
614 (x,0,z) e q2
<=>
(x,0,z) e exp & ~[x=x & 0=0 & z=z]
U Spec, 613
615 [(x,0,z) e q2 => (x,0,z) e exp & ~[x=x & 0=0 & z=z]]
&
[(x,0,z) e exp & ~[x=x & 0=0 & z=z] => (x,0,z) e q2]
Iff-And, 614
616 (x,0,z) e q2 => (x,0,z) e exp & ~[x=x & 0=0 & z=z]
Split, 615
617 (x,0,z) e exp & ~[x=x & 0=0 & z=z] => (x,0,z) e q2
Split, 615
618 ~[(x,0,z) e exp & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q2
Contra, 616
619 ~~[~(x,0,z) e exp | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q2
DeMorgan, 618
620 ~(x,0,z) e exp | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q2
Rem DNeg, 619
Sufficient:
621 ~(x,0,z) e exp | x=x & 0=0 & z=z => ~(x,0,z) e q2
Rem DNeg, 620
622 x=x
Reflex
623 0=0
Reflex
624 z=z
Reflex
625 x=x & 0=0
Join, 622, 623
626 x=x & 0=0 & z=z
Join, 625, 624
627 ~(x,0,z) e exp | x=x & 0=0 & z=z
Arb Or, 626
As Required:
628 ~(x,0,z) e q2
Detach, 621, 627
629 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
Join, 502, 518
630 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
(0,0,x0) e q2
Join, 629, 533
631 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
(0,0,x0) e q2
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]
Join, 630, 555
632 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
(0,0,x0) e q2
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]
Join, 631, 611
633 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
(0,0,x0) e q2
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]
&
~(x,0,z) e q2
Join, 632, 628
634 EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(x,0,z) e d]
E Gen, 633
635 ~(x,0,z) e n3 | EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(x,0,z) e d]
Arb Or, 634
636 ~(x,0,z) e exp
Detach, 499, 635
637 (x,0,z) e exp & ~(x,0,z) e exp
Join, 485, 636
638 ~~[(x,0,z) e exp => z=1]
4 Conclusion, 482
639 (x,0,z) e exp => z=1
Rem DNeg, 638
As Required:
640 ALL(c):[c e n => [(x,0,c) e exp => c=1]]
4 Conclusion, 481
641 z1 e n => [(x,0,z1) e exp => z1=1]
U Spec, 640
642 (x,0,z1) e exp => z1=1
Detach, 641, 463
643 z1=1
Detach, 642, 466
644 z2 e n => [(x,0,z2) e exp => z2=1]
U Spec, 640
645 (x,0,z2) e exp => z2=1
Detach, 644, 464
646 z2=1
Detach, 645, 467
647 z1=z2
Substitute, 646,
643
As Required:
648 ~x=0 => z1=z2
4 Conclusion, 480
649 [x=0 => z1=z2] & [~x=0 => z1=z2]
Join, 479, 648
650 z1=z2
Cases, 468, 649
As Required:
651 (x,0,z1) e exp & (x,0,z2) e exp => z1=z2
4 Conclusion, 465
As Required:
652 ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]]
4 Conclusion, 462
653 0 e n
&
ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,0,c1) e exp & (x,0,c2) e exp => c1=c2]]
Join, 2, 652
As Required:
654 0 e p2
Detach, 461, 653
Prove: ALL(b):[b e p2 => b e n]
Suppose...
655 t e p2
Premise
656 t e p2 <=> t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
U Spec, 456
657 [t e p2 => t e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]]
&
[t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2]
Iff-And, 656
658 t e p2 => t e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
Split, 657
659 t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2
Split, 657
660 t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
Detach, 658, 655
661 t e n
Split, 660
As Required:
662 ALL(b):[b e p2 => b e n]
4 Conclusion, 655
663 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 455, 662
Sufficient: For ALL(b):[b e n => b e p2]
664 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=>
ALL(b):[b e n => b e p2]
Detach, 457, 663
Prove: ALL(b):[b e p2 => b+1 e p2]
Suppose...
665 y e p2
Premise
666 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
U Spec, 456
667 [y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]]
&
[y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]] => y e p2]
Iff-And, 666
668 y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
Split, 667
669 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]] => y e p2
Split, 667
670 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
Detach, 668, 665
671 y e n
Split, 670
672 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
Split, 670
673 ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]
U Spec, 451
674 (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 673
675 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
676 (x,y) e n2 <=> x e n & y e n
U Spec, 675
677 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 676
678 (x,y) e n2 => x e n & y e n
Split, 677
679 x e n & y e n => (x,y) e n2
Split, 677
680 x e n & y e n
Join, 452, 671
681 (x,y) e n2
Detach, 679, 680
682 EXIST(c):[c e n & (x,y,c) e exp]
Detach, 674, 681
683 z e n & (x,y,z) e exp
E Spec, 682
684 z e n
Split, 683
685 (x,y,z) e exp
Split, 683
688
686 ALL(c2):[z e n & c2 e n => [(x,y,z) e exp & (x,y,c2) e exp => z=c2]]
U Spec, 672
687 z' e n
Premise
688 z e n & z' e n => [(x,y,z) e exp & (x,y,z') e exp => z=z']
U Spec, 686
689 z e n & z' e n
Join, 684, 687
690 (x,y,z) e exp & (x,y,z') e exp => z=z'
Detach, 688, 689
691 (x,y,z') e exp
Premise
692 (x,y,z) e exp & (x,y,z') e exp
Join, 685, 691
693 z=z'
Detach, 690, 692
694 (x,y,z') e exp => z=z'
4 Conclusion, 691
695 ALL(c):[c e n => [(x,y,c) e exp => z=c]]
4 Conclusion, 687
Suppose...
696 z' e n
Premise
Suppose to the contrary...
697 ~[(x,y+1,z') e exp => z'=z*x]
Premise
698 ~~[(x,y+1,z') e exp & ~z'=z*x]
Imply-And, 697
699 (x,y+1,z') e exp & ~z'=z*x
Rem DNeg, 698
700 (x,y+1,z') e exp
Split, 699
701 ~z'=z*x
Split, 699
702 ALL(b):ALL(c):[(x,b,c) e exp
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,b,c) e d]]
U Spec, 36
703 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
704 y e n & 1 e n => y+1 e n
U Spec, 703
705 y e n & 1 e n
Join, 671, 3
706 y+1 e n
Detach, 704, 705
707 ALL(c):[(x,y+1,c) e exp
<=>
(x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,c) e d]]
U Spec, 702, 706
708 (x,y+1,z') e exp
<=>
(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d]
U Spec, 707
709 [(x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d]]
&
[(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d] => (x,y+1,z') e exp]
Iff-And, 708
710 (x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d]
Split, 709
711 (x,y+1,z') e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d] => (x,y+1,z') e exp
Split, 709
712 ~[(x,y+1,z') e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d]] => ~(x,y+1,z') e exp
Contra, 710
713 ~~[~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d]] => ~(x,y+1,z') e exp
DeMorgan, 712
714 ~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d] => ~(x,y+1,z') e exp
Rem DNeg, 713
715 ~(x,y+1,z') e n3 | ~~EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d] => ~(x,y+1,z') e exp
Quant, 714
716 ~(x,y+1,z') e n3 | EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(x,y+1,z') e d] => ~(x,y+1,z') e exp
Rem DNeg, 715
717 ~(x,y+1,z') e n3 | EXIST(d):~~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e exp
Imply-And, 716
718 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e exp
Rem DNeg, 717
719 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e exp & ~[a=x & b=y+1 & c=z']]]
Subset, 35
720 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e exp & ~[a=x & b=y+1 & c=z']]
E Spec, 719
717
Define: q
721 Set''(q)
Split, 720
722 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e exp & ~[a=x & b=y+1 & c=z']]
Split, 720
723 (t,u,v) e q
Premise
724 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=x & b=y+1 & c=z']]
U Spec, 722
725 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e exp & ~[t=x & u=y+1 & c=z']]
U Spec, 724
726 (t,u,v) e q
<=>
(t,u,v) e exp & ~[t=x & u=y+1 & v=z']
U Spec, 725
727 [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]
&
[(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]
Iff-And, 726
728 (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']
Split, 727
729 (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 727
730 (t,u,v) e exp & ~[t=x & u=y+1 & v=z']
Detach, 728, 723
731 (t,u,v) e exp
Split, 730
732 ~[t=x & u=y+1 & v=z']
Split, 730
733 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]
U Spec, 61
734 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]
U Spec, 733
735 (t,u,v) e exp => t e n & u e n & v e n
U Spec, 734
736 t e n & u e n & v e n
Detach, 735, 731
As Required:
737 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
4 Conclusion, 723
738 ALL(b):ALL(c):[(0,b,c) e q
<=>
(0,b,c) e exp & ~[0=x & b=y+1 & c=z']]
U Spec, 722
739 ALL(c):[(0,0,c) e q
<=>
(0,0,c) e exp & ~[0=x & 0=y+1 & c=z']]
U Spec, 738
740 (0,0,x0) e q
<=>
(0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']
U Spec, 739
741 [(0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']]
&
[(0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q]
Iff-And, 740
742 (0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']
Split, 741
Sufficient:
743 (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q
Split, 741
744 0=x & 0=y+1 & x0=z'
Premise
745 0=x
Split, 744
746 0=y+1
Split, 744
747 x0=z'
Split, 744
748 y e n => ~y+1=0
U Spec, 8
749 ~y+1=0
Detach, 748, 671
750 y+1=0
Sym, 746
751 y+1=0 & ~y+1=0
Join, 750, 749
As Required:
752 ~[0=x & 0=y+1 & x0=z']
4 Conclusion, 744
753 (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']
Join, 83, 752
As Required:
754 (0,0,x0) e q
Detach, 743, 753
755 t e n
Premise
756 ~t=0
Premise
757 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=x & b=y+1 & c=z']]
U Spec, 722
758 ALL(c):[(t,0,c) e q
<=>
(t,0,c) e exp & ~[t=x & 0=y+1 & c=z']]
U Spec, 757
759 (t,0,1) e q
<=>
(t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']
U Spec, 758
760 [(t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']]
&
[(t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q]
Iff-And, 759
761 (t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']
Split, 760
Sufficient:
762 (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q
Split, 760
763 t e n => [~t=0 => (t,0,1) e exp]
U Spec, 114
764 ~t=0 => (t,0,1) e exp
Detach, 763, 755
765 (t,0,1) e exp
Detach, 764, 756
766 t=x & 0=y+1 & 1=z'
Premise
767 t=x
Split, 766
768 0=y+1
Split, 766
769 1=z'
Split, 766
770 y e n => ~y+1=0
U Spec, 8
771 ~y+1=0
Detach, 770, 671
772 ~0=y+1
Sym, 771
773 0=y+1 & ~0=y+1
Join, 768, 772
774 ~[t=x & 0=y+1 & 1=z']
4 Conclusion, 766
775 (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']
Join, 765, 774
776 (t,0,1) e q
Detach, 762, 775
777 ~t=0 => (t,0,1) e q
4 Conclusion, 756
As Required:
778 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 755
779 (t,u,v) e q
Premise
780 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=x & b=y+1 & c=z']]
U Spec, 722
781 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e exp & ~[t=x & u=y+1 & c=z']]
U Spec, 780
782 (t,u,v) e q
<=>
(t,u,v) e exp & ~[t=x & u=y+1 & v=z']
U Spec, 781
783 [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]
&
[(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]
Iff-And, 782
784 (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']
Split, 783
785 (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 783
786 (t,u,v) e exp & ~[t=x & u=y+1 & v=z']
Detach, 784, 779
787 (t,u,v) e exp
Split, 786
788 ~[t=x & u=y+1 & v=z']
Split, 786
789 ALL(b):ALL(c):[(t,b,c) e exp
<=>
(t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,b,c) e d]]
U Spec, 36
790 ALL(c):[(t,u,c) e exp
<=>
(t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,c) e d]]
U Spec, 789
791 (t,u,v) e exp
<=>
(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
U Spec, 790
792 [(t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp]
Iff-And, 791
793 (t,u,v) e exp => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 792
794 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d] => (t,u,v) e exp
Split, 792
795 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Detach, 793, 787
796 (t,u,v) e n3
Split, 795
797 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=>
(t,u,v) e d]
Split, 795
798 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 32
799 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 798
800 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 799
801 [(t,u,v) e n3 => t e n & u e n & v e n]
&
[t e n & u e n & v e n => (t,u,v) e n3]
Iff-And, 800
802 (t,u,v) e n3 => t e n & u e n & v e n
Split, 801
803 t e n & u e n & v e n => (t,u,v) e n3
Split, 801
804 t e n & u e n & v e n
Detach, 802, 796
805 t e n
Split, 804
806 u e n
Split, 804
807 v e n
Split, 804
808 ALL(b):[u e n & b e n => u+b e n]
U Spec, 6
809 u e n & 1 e n => u+1 e n
U Spec, 808
810 u e n & 1 e n
Join, 806, 3
811 u+1 e n
Detach, 809, 810
812 ALL(b):[v e n & b e n => v*b e n]
U Spec, 10
813 v e n & t e n => v*t e n
U Spec, 812
814 v e n & t e n
Join, 807, 805
815 v*t e n
Detach, 813, 814
816 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e exp & ~[t=x & b=y+1 & c=z']]
U Spec, 722
817 ALL(c):[(t,u+1,c) e q
<=>
(t,u+1,c) e exp & ~[t=x & u+1=y+1 & c=z']]
U Spec, 816, 811
818 (t,u+1,v*t) e q
<=>
(t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']
U Spec, 817, 815
819 [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']]
&
[(t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q]
Iff-And, 818
820 (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']
Split, 819
Sufficient:
821 (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q
Split, 819
822 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e exp => (t,b+1,c*t) e exp]]
U Spec, 168
823 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e exp => (t,u+1,c*t) e exp]]
U Spec, 822
824 t e n & u e n & v e n
=>
[(t,u,v) e exp => (t,u+1,v*t) e exp]
U Spec, 823
825 (t,u,v) e exp => (t,u+1,v*t) e exp
Detach, 824, 804
826 (t,u+1,v*t) e exp
Detach, 825, 787
827 t=x & u+1=y+1 & v*t=z'
Premise
828 t=x
Split, 827
829 u+1=y+1
Split, 827
830 v*t=z'
Split, 827
831 v*x=z'
Substitute, 828,
830
832 ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]
U Spec, 7
833 ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]
U Spec, 832
834 u e n & 1 e n & y e n => [u+1=y+1 => u=y]
U Spec, 833
835 u e n & 1 e n
Join, 806, 3
836 u e n & 1 e n & y e n
Join, 835, 671
837 u+1=y+1 => u=y
Detach, 834, 836
829
838 u=y
Detach, 837, 829
839 (x,u,v) e exp
Substitute, 828,
787
840 (x,y,v) e exp
Substitute, 838,
839
841 v e n => [(x,y,v) e exp => z=v]
U Spec, 695
842 (x,y,v) e exp => z=v
Detach, 841, 807
834
843 z=v
Detach, 842, 840
844 z*x=z'
Substitute, 843,
831
845 z'=z*x
Sym, 844
846 z'=z*x & ~z'=z*x
Join, 845, 701
847 ~[t=x & u+1=y+1 & v*t=z']
4 Conclusion, 827
848 (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']
Join, 826, 847
849 (t,u+1,v*t) e q
Detach, 821, 848
850 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 779
851 ALL(b):ALL(c):[(x,b,c) e q
<=>
(x,b,c) e exp & ~[x=x & b=y+1 & c=z']]
U Spec, 722
852 ALL(c):[(x,y+1,c) e q
<=>
(x,y+1,c) e exp & ~[x=x & y+1=y+1 & c=z']]
U Spec, 851, 706
853 (x,y+1,z') e q
<=>
(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']
U Spec, 852
854 [(x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']]
&
[(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q]
Iff-And, 853
855 (x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']
Split, 854
856 (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q
Split, 854
857 ~[(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
Contra, 855
858 ~~[~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
DeMorgan, 857
859 ~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q
Rem DNeg, 858
860 ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q
Rem DNeg, 859
861 x=x
Reflex
862 y+1=y+1
Reflex, 706
863 z'=z'
Reflex
864 x=x & y+1=y+1
Join, 861, 862
865 x=x & y+1=y+1 & z'=z'
Join, 864, 863
866 ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z'
Arb Or, 865
As Required:
867 ~(x,y+1,z') e q
Detach, 860, 866
868 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
Join, 721, 737
869 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
Join, 868, 754
870 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 869, 778
871 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Join, 870, 850
872 Set''(q)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]
&
(0,0,x0) e q
&
ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
&
~(x,y+1,z') e q
Join, 871, 867
873 EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(x,y+1,z') e d]
E Gen, 872
874 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
(0,0,x0) e d
&
ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
&
~(x,y+1,z') e d]
Arb Or, 873
875 ~(x,y+1,z') e exp
Detach, 718, 874
876 ~(x,y+1,z') e exp & (x,y+1,z') e exp
Join, 875, 700
877 ~~[(x,y+1,z') e exp => z'=z*x]
4 Conclusion, 697
878 (x,y+1,z') e exp => z'=z*x
Rem DNeg, 877
879 ALL(d):[d e n => [(x,y+1,d) e exp => d=z*x]]
4 Conclusion, 696
880 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
881 y e n & 1 e n => y+1 e n
U Spec, 880
882 y e n & 1 e n
Join, 671, 3
883 y+1 e n
Detach, 881, 882
884 y+1 e p2 <=> y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]
U Spec, 456, 883
885 [y+1 e p2 => y+1 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]]
&
[y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]] => y+1 e p2]
Iff-And, 884
886 y+1 e p2 => y+1 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]
Split, 885
Sufficient:
887 y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]] => y+1 e p2
Split, 885
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,y+1,c1) e exp & (x,y+1,c2) e exp =>
c1=c2]]
Suppose...
888 z1 e n & z2 e n
Premise
889 z1 e n
Split, 888
890 z2 e n
Split, 888
Prove: (x,y+1,z1) e exp & (x,y+1,z2) e exp =>
z1=z2
Suppose...
891 (x,y+1,z1) e exp & (x,y+1,z2) e exp
Premise
892 (x,y+1,z1) e exp
Split, 891
893 (x,y+1,z2) e exp
Split, 891
894 z1 e n => [(x,y+1,z1) e exp => z1=z*x]
U Spec, 879
895 (x,y+1,z1) e exp => z1=z*x
Detach, 894, 889
896 z1=z*x
Detach, 895, 892
897 z2 e n => [(x,y+1,z2) e exp => z2=z*x]
U Spec, 879
898 (x,y+1,z2) e exp => z2=z*x
Detach, 897, 890
899 z2=z*x
Detach, 898, 893
900 z1=z2
Substitute, 899,
896
As Required:
901 (x,y+1,z1) e exp & (x,y+1,z2) e exp => z1=z2
4 Conclusion, 891
As Required:
902 ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]
4 Conclusion, 888
903 y+1 e n
&
ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]
Join, 883, 902
904 y+1 e p2
Detach, 887, 903
As Required:
905 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 665
906 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 654, 905
907 ALL(b):[b e n => b e p2]
Detach, 664, 906
908 t e n
Premise
909 t e n => t e p2
U Spec, 907
910 t e p2
Detach, 909, 908
911 t e p2 <=> t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
U Spec, 456
912 [t e p2 => t e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]]
&
[t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2]
Iff-And, 911
913 t e p2 => t e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
Split, 912
914 t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2
Split, 912
915 t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
Detach, 913, 910
916 t e n
Split, 915
917 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]
Split, 915
918 ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]
4 Conclusion, 908
As Required:
919 ALL(a):[a e n
=>
ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e exp & (a,b,c2) e exp => c1=c2]]]]
4 Conclusion, 452
Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp & (a1,a2,b2) e exp =>
b1=b2]]
Suppose...
920 (x,y) e n2 & z1 e n & z2 e n
Premise
921 (x,y) e n2
Split, 920
922 z1 e n
Split, 920
923 z2 e n
Split, 920
924 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
925 (x,y) e n2 <=> x e n & y e n
U Spec, 924
926 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 925
927 (x,y) e n2 => x e n & y e n
Split, 926
928 x e n & y e n => (x,y) e n2
Split, 926
929 x e n & y e n
Detach, 927, 921
930 x e n
Split, 929
931 y e n
Split, 929
932 x e n
=>
ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]
U Spec, 919
933 ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]
Detach, 932, 930
934 y e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
U Spec, 933
935 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e exp & (x,y,c2) e exp => c1=c2]]
Detach, 934, 931
936 ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e exp & (x,y,c2) e exp => z1=c2]]
U Spec, 935
937 z1 e n & z2 e n => [(x,y,z1) e exp & (x,y,z2) e exp => z1=z2]
U Spec, 936
938 z1 e n & z2 e n
Join, 922, 923
939 (x,y,z1) e exp & (x,y,z2) e exp => z1=z2
Detach, 937, 938
Functionality, Part 3
940 ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]
4 Conclusion, 920
941 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]
Join, 347, 451
942 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]
Join, 941, 940
exp is a binary function on n
943 ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]
Detach, 43, 942
ESTABLISH REQUIRED PROPERTIES OF exp
************************************
944 ALL(a2):ALL(b):[(0,a2) e n2 & b e n => [exp(0,a2)=b <=> (0,a2,b) e exp]]
U Spec, 943
945 ALL(b):[(0,0) e n2 & b e n => [exp(0,0)=b <=> (0,0,b) e exp]]
U Spec, 944
Prove: exp(0,0)=x0
946 (0,0) e n2 & x0 e n => [exp(0,0)=x0 <=> (0,0,x0) e exp]
U Spec, 945
947 ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]
U Spec, 22
948 (0,0) e n2 <=> 0 e n & 0 e n
U Spec, 947
949 [(0,0) e n2 => 0 e n & 0 e n]
&
[0 e n & 0 e n => (0,0) e n2]
Iff-And, 948
950 (0,0) e n2 => 0 e n & 0 e n
Split, 949
951 0 e n & 0 e n => (0,0) e n2
Split, 949
952 0 e n & 0 e n
Join, 2, 2
953 (0,0) e n2
Detach, 951, 952
954 (0,0) e n2 & x0 e n
Join, 953, 14
955 exp(0,0)=x0 <=> (0,0,x0) e exp
Detach, 946, 954
956 [exp(0,0)=x0 => (0,0,x0) e exp]
&
[(0,0,x0) e exp => exp(0,0)=x0]
Iff-And, 955
957 exp(0,0)=x0 => (0,0,x0) e exp
Split, 956
958 (0,0,x0) e exp => exp(0,0)=x0
Split, 956
As Required:
959 exp(0,0)=x0
Detach, 958, 83
Prove: ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Suppose...
960 x e n & y e n
Premise
961 x e n
Split, 960
962 y e n
Split, 960
963 ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]
U Spec, 451
964 (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 963
965 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
966 (x,y) e n2 <=> x e n & y e n
U Spec, 965
967 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 966
968 (x,y) e n2 => x e n & y e n
Split, 967
969 x e n & y e n => (x,y) e n2
Split, 967
970 (x,y) e n2
Detach, 969, 960
971 EXIST(c):[c e n & (x,y,c) e exp]
Detach, 964, 970
972 z e n & (x,y,z) e exp
E Spec, 971
973 z e n
Split, 972
974 (x,y,z) e exp
Split, 972
975 ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]
U Spec, 943
976 ALL(b):[(x,y) e n2 & b e n => [exp(x,y)=b <=> (x,y,b) e exp]]
U Spec, 975
977 (x,y) e n2 & z e n => [exp(x,y)=z <=> (x,y,z) e exp]
U Spec, 976
978 (x,y) e n2 & z e n
Join, 970, 973
979 exp(x,y)=z <=> (x,y,z) e exp
Detach, 977, 978
980 [exp(x,y)=z => (x,y,z) e exp]
&
[(x,y,z) e exp => exp(x,y)=z]
Iff-And, 979
981 exp(x,y)=z => (x,y,z) e exp
Split, 980
982 (x,y,z) e exp => exp(x,y)=z
Split, 980
983 exp(x,y)=z
Detach, 982, 974
984 exp(x,y) e n
Substitute, 983,
973
As Required:
985 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
4 Conclusion, 960
Prove: ALL(a):[a e n => [~a=0
=> exp(a,0)=1]]
Suppose..
986 x e n
Premise
Prove: ~x=0 => exp(x,0)=1
Suppose...
987 ~x=0
Premise
988 x e n => [~x=0 => (x,0,1) e exp]
U Spec, 114
989 ~x=0 => (x,0,1) e exp
Detach, 988, 986
990 (x,0,1) e exp
Detach, 989, 987
991 ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]
U Spec, 943
992 ALL(b):[(x,0) e n2 & b e n => [exp(x,0)=b <=> (x,0,b) e exp]]
U Spec, 991
993 (x,0) e n2 & 1 e n => [exp(x,0)=1 <=> (x,0,1) e exp]
U Spec, 992
994 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
995 (x,0) e n2 <=> x e n & 0 e n
U Spec, 994
996 [(x,0) e n2 => x e n & 0 e n]
&
[x e n & 0 e n => (x,0) e n2]
Iff-And, 995
997 (x,0) e n2 => x e n & 0 e n
Split, 996
998 x e n & 0 e n => (x,0) e n2
Split, 996
999 x e n & 0 e n
Join, 986, 2
1000 (x,0) e n2
Detach, 998, 999
1001 (x,0) e n2 & 1 e n
Join, 1000, 3
1002 exp(x,0)=1 <=> (x,0,1) e exp
Detach, 993, 1001
1003 [exp(x,0)=1 => (x,0,1) e exp]
&
[(x,0,1) e exp => exp(x,0)=1]
Iff-And, 1002
1004 exp(x,0)=1 => (x,0,1) e exp
Split, 1003
1005 (x,0,1) e exp => exp(x,0)=1
Split, 1003
1006 exp(x,0)=1
Detach, 1005, 990
As Required:
1007 ~x=0 => exp(x,0)=1
4 Conclusion, 987
As Required:
1008 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
4 Conclusion, 986
Prove: ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Suppose...
1009 x e n & y e n
Premise
1010 x e n
Split, 1009
1011 y e n
Split, 1009
1012 ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]
U Spec, 451
1013 (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]
U Spec, 1012
1014 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
1015 (x,y) e n2 <=> x e n & y e n
U Spec, 1014
1016 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 1015
1017 (x,y) e n2 => x e n & y e n
Split, 1016
1018 x e n & y e n => (x,y) e n2
Split, 1016
1019 (x,y) e n2
Detach, 1018,
1009
1020 EXIST(c):[c e n & (x,y,c) e exp]
Detach, 1013,
1019
1021 z e n & (x,y,z) e exp
E Spec, 1020
1022 z e n
Split, 1021
1023 (x,y,z) e exp
Split, 1021
1024 ALL(b):ALL(c):[x e n & b e n & c e n
=>
[(x,b,c) e exp => (x,b+1,c*x) e exp]]
U Spec, 168
1025 ALL(c):[x e n & y e n & c e n
=>
[(x,y,c) e exp => (x,y+1,c*x) e exp]]
U Spec, 1024
1026 x e n & y e n & z e n
=>
[(x,y,z) e exp => (x,y+1,z*x) e exp]
U Spec, 1025
1027 x e n & y e n & z e n
Join, 1009, 1022
1028 (x,y,z) e exp => (x,y+1,z*x) e exp
Detach, 1026,
1027
1029 (x,y+1,z*x) e exp
Detach, 1028,
1023
1030 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
1031 y e n & 1 e n => y+1 e n
U Spec, 1030
1032 y e n & 1 e n
Join, 1011, 3
1033 y+1 e n
Detach, 1031,
1032
1034 ALL(b):[z e n & b e n => z*b e n]
U Spec, 10
1035 z e n & x e n => z*x e n
U Spec, 1034
1036 z e n & x e n
Join, 1022, 1010
1037 z*x e n
Detach, 1035,
1036
1038 ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]
U Spec, 943
1039 ALL(b):[(x,y) e n2 & b e n => [exp(x,y)=b <=> (x,y,b) e exp]]
U Spec, 1038
1040 (x,y) e n2 & z e n => [exp(x,y)=z <=> (x,y,z) e exp]
U Spec, 1039
1041 (x,y) e n2 & z e n
Join, 1019, 1022
1042 exp(x,y)=z <=> (x,y,z) e exp
Detach, 1040,
1041
1043 [exp(x,y)=z => (x,y,z) e exp]
&
[(x,y,z) e exp => exp(x,y)=z]
Iff-And, 1042
1044 exp(x,y)=z => (x,y,z) e exp
Split, 1043
1045 (x,y,z) e exp => exp(x,y)=z
Split, 1043
1046 exp(x,y)=z
Detach, 1045,
1023
1047 ALL(b):[(x,y+1) e n2 & b e n => [exp(x,y+1)=b <=> (x,y+1,b) e exp]]
U Spec, 1038,
1033
1048 (x,y+1) e n2 & z*x e n => [exp(x,y+1)=z*x <=> (x,y+1,z*x) e exp]
U Spec, 1047,
1037
1049 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 22
1050 (x,y+1) e n2 <=> x e n & y+1 e n
U Spec, 1049,
1033
1051 [(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, 1050
1052 (x,y+1) e n2 => x e n & y+1 e n
Split, 1051
1053 x e n & y+1 e n => (x,y+1) e n2
Split, 1051
1054 x e n & y+1 e n
Join, 1010, 1033
1055 (x,y+1) e n2
Detach, 1053,
1054
1056 (x,y+1) e n2 & z*x e n
Join, 1055, 1037
1057 exp(x,y+1)=z*x <=> (x,y+1,z*x) e exp
Detach, 1048,
1056
1058 [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, 1057
1059 exp(x,y+1)=z*x => (x,y+1,z*x) e exp
Split, 1058
1060 (x,y+1,z*x) e exp => exp(x,y+1)=z*x
Split, 1058
1061 exp(x,y+1)=z*x
Detach, 1060,
1029
1062 exp(x,y+1)=exp(x,y)*x
Substitute, 1046,
1061
As Required:
1063 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
4 Conclusion, 1009
1064 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
Join, 985, 959
1065 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]]
Join, 1064, 1008
1066 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]
Join, 1065, 1063
As Required:
1067 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]]]
4 Conclusion, 14