THEOREM
*******
From Peano's
Axiom, we have:
EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]]
where
n = the set of natural numbers
add = the add function
next = the successor function
on n
COROLARY
********
add(1,1)=2
OUTLINE
*******
1. Peano’s
Axioms (lines
1-6)
2. Construct n3, the set of
ordered triples of n (lines 7-16)
3. Construct pn3, the power set
of n3 (lines 17-22)
4. Construct add, a subset of n3 (lines 23-26)
5. Prove that add is a function
with the required properties (lines 27-740)
6. Prove add(1,1)=2 (lines 741-760)
This formal proof was written
and machine-verified with the aid of the author’s DC Proof 2.0 software
available at http://www.dcproof.com
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
2 0 e n
Axiom
next is a function on n
3 ALL(a):[a e n => next(a) e n]
Axiom
next is an injective (1-to-1)
function
4 ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Axiom
0 has no predecessor
5 ALL(a):[a e n => ~next(a)=0]
Axiom
Principle of mathematical
induction (PMI)
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => next(b) e a]
=>
ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Construct the set of ordered
triples of n
Apply the Cartesian Product
Axiom
7 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
8 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, 7
9 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, 8
10 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, 9
11 Set(n) & Set(n)
Join, 1, 1
12 Set(n) & Set(n) & Set(n)
Join, 11, 1
13 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, 10, 12
14 Set''(n3) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 13
Define: n3 (the set of ordered triples of n)
**********
15 Set''(n3)
Split, 14
16 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 14
Construct the powerset of n3
Apply the Power Set Axiom
17 ALL(a):[Set''(a)
=> EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e a]]]]
Power Set
18 Set''(n3) =>
EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
U Spec, 17
19 EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
Detach, 18, 15
20 Set(pn3)
&
ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
E Spec, 19
Define: pn3 (the power set of n3)
***********
21 Set(pn3)
Split, 20
22 ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
Split, 20
Construct the set add
Apply the Subset Axiom
23 EXIST(sub):[Set''(sub)
& ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(a,b,c) e d]]]
Subset, 15
24 Set''(add) &
ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=>
(a,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(a,b,c) e d]]
E Spec, 23
Define: add
***********
25 Set''(add)
Split, 24
26 ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=>
(a,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(a,b,c) e d]]
Split, 24
Derive some useful properties of add
************************************
Prove: ALL(a):[a e n =>
(a,0,a) e add]
Suppose...
27 x e n
Premise
28 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
29 ALL(c):[(x,0,c) e add
<=>
(x,0,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,c) e d]]
U Spec, 28
30 (x,0,x) e add
<=>
(x,0,x) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d]
U Spec, 29
31 [(x,0,x) e add => (x,0,x) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d]]
&
[(x,0,x) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d] => (x,0,x) e add]
Iff-And, 30
32 (x,0,x) e add => (x,0,x) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d]
Split, 31
Sufficient: (x,0,x) e add
33 (x,0,x) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d] => (x,0,x) e add
Split, 31
34 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
35 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 34
36 (x,0,x) e n3 <=> x e n & 0 e n & x e n
U Spec, 35
37 [(x,0,x) e n3 => x e n & 0 e n & x e n]
&
[x e n & 0 e n & x e n => (x,0,x) e n3]
Iff-And, 36
38 (x,0,x) e n3 => x e n & 0 e n & x e n
Split, 37
39 x e n & 0 e n & x e n => (x,0,x) e n3
Split, 37
40 x e n & 0 e n
Join, 27, 2
41 x e n & 0 e n & x e n
Join, 40, 27
42 (x,0,x) e n3
Detach, 39, 41
Prove: ALL(d):[d e pn3
& ALL(e):[e
e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=> (x,0,x) e d]
Suppose...
43 q e pn3
&
ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Premise
44 q e pn3
Split, 43
45 ALL(e):[e e n => (e,0,e) e q]
Split, 43
46 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Split, 43
47 x e n => (x,0,x) e q
U Spec, 45
48 (x,0,x) e q
Detach, 47, 27
As Required:
49 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d]
4 Conclusion, 43
50 (x,0,x) e n3
&
ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,x) e d]
Join, 42, 49
51 (x,0,x) e add
Detach, 33, 50
As Required:
52 ALL(a):[a e n => (a,0,a) e add]
4 Conclusion, 27
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [(a,b,c) e add => (a,next(b),next(c)) e add]]
Suppose...
53 x e n & y e n & z e n
Premise
54 x e n
Split, 53
55 y e n
Split, 53
56 z e n
Split, 53
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [(a,b,c) e add => (a,next(b),next(c)) e add]]
Suppose...
57 (x,y,z) e add
Premise
58 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
59 ALL(c):[(x,y,c) e add
<=>
(x,y,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,c) e d]]
U Spec, 58
60 (x,y,z) e add
<=>
(x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
U Spec, 59
61 [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add]
Iff-And, 60
62 (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Split, 61
63 (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add
Split, 61
64 (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Detach, 62, 57
65 (x,y,z) e n3
Split, 64
66 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Split, 64
67 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
68 ALL(c):[(x,next(y),c) e add
<=>
(x,next(y),c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),c) e d]]
U Spec, 67
69 (x,next(y),next(z)) e add
<=>
(x,next(y),next(z)) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d]
U Spec, 68
70 [(x,next(y),next(z)) e add => (x,next(y),next(z)) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d]]
&
[(x,next(y),next(z)) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d] => (x,next(y),next(z)) e add]
Iff-And, 69
71 (x,next(y),next(z)) e add => (x,next(y),next(z)) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d]
Split, 70
Sufficient: (x,next(y),next(z)) e add
72 (x,next(y),next(z)) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d] => (x,next(y),next(z)) e add
Split, 70
73 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
74 ALL(c3):[(x,next(y),c3) e n3 <=> x e n & next(y) e n & c3 e n]
U Spec, 73
75 (x,next(y),next(z)) e n3 <=> x e n & next(y) e n & next(z) e n
U Spec, 74
76 [(x,next(y),next(z)) e n3 => x e n & next(y) e n & next(z) e n]
&
[x e n & next(y) e n & next(z) e n => (x,next(y),next(z)) e n3]
Iff-And, 75
77 (x,next(y),next(z)) e n3 => x e n & next(y) e n & next(z) e n
Split, 76
78 x e n & next(y) e n & next(z) e n => (x,next(y),next(z)) e n3
Split, 76
79 y e n => next(y) e n
U Spec, 3
80 next(y) e n
Detach, 79, 55
81 z e n => next(z) e n
U Spec, 3
82 next(z) e n
Detach, 81, 56
83 x e n & next(y) e n
Join, 54, 80
84 x e n & next(y) e n & next(z) e n
Join, 83, 82
85 (x,next(y),next(z)) e n3
Detach, 78, 84
Prove: ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=> (x,next(y),next(z)) e d]
Suppose...
86 q e pn3
&
ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Premise
87 q e pn3
Split, 86
88 ALL(e):[e e n => (e,0,e) e q]
Split, 86
89 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Split, 86
90 ALL(f):ALL(g):[(x,f,g) e q => (x,next(f),next(g)) e q]
U Spec, 89
91 ALL(g):[(x,y,g) e q => (x,next(y),next(g)) e q]
U Spec, 90
Sufficient: (x,next(y),next(z))
e q
92 (x,y,z) e q => (x,next(y),next(z)) e q
U Spec, 91
Sufficient: (x,y,z) e q
93 q e pn3
&
ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
=>
(x,y,z) e q
U Spec, 66
94 (x,y,z) e q
Detach, 93, 86
95 (x,next(y),next(z)) e q
Detach, 92, 94
As Required:
96 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d]
4 Conclusion, 86
97 (x,next(y),next(z)) e n3
&
ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),next(z)) e d]
Join, 85, 96
98 (x,next(y),next(z)) e add
Detach, 72, 97
As Required:
99 (x,y,z) e add => (x,next(y),next(z)) e add
4 Conclusion, 57
As Required:
100 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=>
[(a,b,c) e add => (a,next(b),next(c)) e add]]
4 Conclusion, 53
Prove: ALL(a):[aen => ALL(b):[ben =>
[(a,0,b)eadd => b=a]]]
Suppose...
101 x e n
Premise
Prove: ALL(b):[b e n =>
[(x,0,b) e add => b=x]]
Suppose...
102 z e n
Premise
Prove: (x,0,z) e add &
~z=x
Suppose to the contrary...
103 (x,0,z) e add & ~z=x
Premise
104 (x,0,z) e add
Split, 103
105 ~z=x
Split, 103
106 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
107 ALL(c):[(x,0,c) e add
<=>
(x,0,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,c) e d]]
U Spec, 106
108 (x,0,z) e add
<=>
(x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d]
U Spec, 107
109 [(x,0,z) e add => (x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d]]
&
[(x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d] => (x,0,z) e add]
Iff-And, 108
110 (x,0,z) e add => (x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d]
Split, 109
111 (x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d] => (x,0,z) e add
Split, 109
112 ~[(x,0,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,0,z) e d]] => ~(x,0,z) e add
Contra, 110
113 ~[(x,0,z) e n3 & ALL(d):~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d]] => ~(x,0,z) e add
Imply-And, 112
114 ~~[~(x,0,z) e n3 | ~ALL(d):~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d]] => ~(x,0,z) e add
DeMorgan, 113
115 ~(x,0,z) e n3 | ~ALL(d):~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 114
116 ~(x,0,z) e n3 | ~~EXIST(d):~~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Quant, 115
117 ~(x,0,z) e n3 | EXIST(d):~~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 116
Sufficient: ~(x,0,z) e add (to obtain a contradiction)
Use d=q as defined below
118 ~(x,0,z) e n3 | EXIST(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 117
119 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]]
Subset, 25
120 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]
E Spec, 119
Define: q
*********
121 Set''(q)
Split, 120
122 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]
Split, 120
123 q e pn3 <=> Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
U Spec, 22
124 [q e pn3 => Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]]
&
[Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]
Iff-And, 123
125 q e pn3 => Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
Split, 124
Sufficient: q e pn3
126 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 124
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Suppose...
127 (t,u,v) e q
Premise
128 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 122
129 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 128
130 (t,u,v) e q
<=>
(t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 129
131 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q]
Iff-And, 130
132 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 131
133 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 131
134 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 132, 127
135 (t,u,v) e add
Split, 134
136 ~[t=x & u=0 & v=z]
Split, 134
137 ALL(b):ALL(c):[(t,b,c) e add
<=>
(t,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,b,c) e d]]
U Spec, 26
138 ALL(c):[(t,u,c) e add
<=>
(t,u,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,c) e d]]
U Spec, 137
139 (t,u,v) e add
<=>
(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
U Spec, 138
140 [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add]
Iff-And, 139
141 (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 140
142 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add
Split, 140
143 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Detach, 141, 135
144 (t,u,v) e n3
Split, 143
145 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
4 Conclusion, 127
146 Set''(q)
&
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
Join, 121, 145
As Required:
147 q e pn3
Detach, 126, 146
Prove: ALL(e):[e e n =>
(e,0,e) e q]
Suppose...
148 t e n
Premise
149 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 122
150 ALL(c):[(t,0,c) e q
<=>
(t,0,c) e add & ~[t=x & 0=0 & c=z]]
U Spec, 149
151 (t,0,t) e q
<=>
(t,0,t) e add & ~[t=x & 0=0 & t=z]
U Spec, 150
152 [(t,0,t) e q => (t,0,t) e add & ~[t=x & 0=0 & t=z]]
&
[(t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q]
Iff-And, 151
153 (t,0,t) e q => (t,0,t) e add & ~[t=x & 0=0 & t=z]
Split, 152
Sufficient: (t,0,t) e q
154 (t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q
Split, 152
155 t e n => (t,0,t) e add
U Spec, 52
156 (t,0,t) e add
Detach, 155, 148
Prove: ~[t=x & 0=0 & t=z]
Suppose to the contrary...
157 t=x & 0=0 & t=z
Premise
158 t=x
Split, 157
159 0=0
Split, 157
160 t=z
Split, 157
161 z=x
Substitute, 160,
158
Obtain the contradiction...
162 z=x & ~z=x
Join, 161, 105
As Required:
163 ~[t=x & 0=0 & t=z]
4 Conclusion, 157
164 (t,0,t) e add & ~[t=x & 0=0 & t=z]
Join, 156, 163
165 (t,0,t) e q
Detach, 154, 164
As Required:
166 ALL(e):[e e n => (e,0,e) e q]
4 Conclusion, 148
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g)
eq => (e,next(f),next(g)) e q]
Suppose...
167 (t,u,v) e q
Premise
168 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 122
169 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 168
170 (t,u,v) e q
<=>
(t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 169
171 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q]
Iff-And, 170
172 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 171
173 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 171
174 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 172, 167
175 (t,u,v) e add
Split, 174
176 ~[t=x & u=0 & v=z]
Split, 174
177 ALL(b):ALL(c):[(t,b,c) e add
<=>
(t,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,b,c) e d]]
U Spec, 26
178 ALL(c):[(t,u,c) e add
<=>
(t,u,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,c) e d]]
U Spec, 177
179 (t,u,v) e add
<=>
(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
U Spec, 178
180 [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add]
Iff-And, 179
181 (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 180
182 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add
Split, 180
183 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Detach, 181, 175
184 (t,u,v) e n3
Split, 183
185 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 183
186 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 122
187 ALL(c):[(t,next(u),c) e q
<=>
(t,next(u),c) e add & ~[t=x & next(u)=0 & c=z]]
U Spec, 186
188 (t,next(u),next(v)) e q
<=>
(t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]
U Spec, 187
189 [(t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]]
&
[(t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z] => (t,next(u),next(v)) e q]
Iff-And, 188
190 (t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]
Split, 189
Sufficient: (t,next(u),next(v))
e q
191 (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z] => (t,next(u),next(v)) e q
Split, 189
192 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e add => (t,next(b),next(c)) e add]]
U Spec, 100
193 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e add => (t,next(u),next(c)) e add]]
U Spec, 192
194 t e n & u e n & v e n
=>
[(t,u,v) e add => (t,next(u),next(v)) e add]
U Spec, 193
195 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 16
196 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 195
197 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 196
198 [(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, 197
199 (t,u,v) e n3 => t e n & u e n & v e n
Split, 198
200 t e n & u e n & v e n => (t,u,v) e n3
Split, 198
201 t e n & u e n & v e n
Detach, 199, 184
202 t e n
Split, 201
203 u e n
Split, 201
204 v e n
Split, 201
205 (t,u,v) e add => (t,next(u),next(v)) e add
Detach, 194, 201
As Required:
206 (t,next(u),next(v)) e add
Detach, 205, 175
Prove: ~[t=x & next(u)=0 & next(v)=z]
Suppose to the contrary...
207 t=x & next(u)=0 & next(v)=z
Premise
208 t=x
Split, 207
209 next(u)=0
Split, 207
210 next(v)=z
Split, 207
211 u e n => ~next(u)=0
U Spec, 5
212 ~next(u)=0
Detach, 211, 203
Obtain the contradiction...
213 next(u)=0 & ~next(u)=0
Join, 209, 212
As Required:
214 ~[t=x & next(u)=0 & next(v)=z]
4 Conclusion, 207
215 (t,next(u),next(v)) e add
&
~[t=x & next(u)=0 & next(v)=z]
Join, 206, 214
216 (t,next(u),next(v)) e q
Detach, 191, 215
As Required:
217 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
4 Conclusion, 167
218 ALL(b):ALL(c):[(x,b,c) e q
<=>
(x,b,c) e add & ~[x=x & b=0 & c=z]]
U Spec, 122
219 ALL(c):[(x,0,c) e q
<=>
(x,0,c) e add & ~[x=x & 0=0 & c=z]]
U Spec, 218
220 (x,0,z) e q
<=>
(x,0,z) e add & ~[x=x & 0=0 & z=z]
U Spec, 219
221 [(x,0,z) e q => (x,0,z) e add & ~[x=x & 0=0 & z=z]]
&
[(x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q]
Iff-And, 220
222 (x,0,z) e q => (x,0,z) e add & ~[x=x & 0=0 & z=z]
Split, 221
223 (x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q
Split, 221
224 ~[(x,0,z) e add & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
Contra, 222
225 ~~[~(x,0,z) e add | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
DeMorgan, 224
226 ~(x,0,z) e add | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q
Rem DNeg, 225
227 ~(x,0,z) e add | x=x & 0=0 & z=z => ~(x,0,z) e q
Rem DNeg, 226
228 x=x
Reflex
229 0=0
Reflex
230 z=z
Reflex
231 x=x & 0=0
Join, 228, 229
232 x=x & 0=0 & z=z
Join, 231, 230
233 ~(x,0,z) e add | x=x & 0=0 & z=z
Arb Or, 232
As Required:
234 ~(x,0,z) e q
Detach, 227, 233
235 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
Join, 147, 166
236 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Join, 235, 217
237 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
&
~(x,0,z) e q
Join, 236, 234
238 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
&
~(x,0,z) e d]
E Gen, 237
239 ~(x,0,z) e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
&
~(x,0,z) e d]
Arb Or, 238
240 ~(x,0,z) e add
Detach, 118, 239
241 (x,0,z) e add & ~(x,0,z) e add
Join, 104, 240
As Required:
242 ~[(x,0,z) e add & ~z=x]
4 Conclusion, 103
243 ~~[(x,0,z) e add => ~~z=x]
Imply-And, 242
244 (x,0,z) e add => ~~z=x
Rem DNeg, 243
245 (x,0,z) e add => z=x
Rem DNeg, 244
As Required:
246 ALL(b):[b e n => [(x,0,b) e add => b=x]]
4 Conclusion, 102
As Required:
247 ALL(a):[a e n => ALL(b):[b e n => [(a,0,b) e add => b=a]]]
4 Conclusion, 101
248 ALL(f):ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => c1 e a1 & c2 e a2 & d e b]
&
ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b &
(c1,c2,d) e f]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f &
(c1,c2,d2) e f => d1=d2]
=>
ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]
Function
249 ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e a1 & c2 e a2 & d e b]
&
ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b &
(c1,c2,d) e add]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add &
(c1,c2,d2) e add => d1=d2]
=>
ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 248
250 ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e a2 & d e b]
&
ALL(c1):ALL(c2):[c1 e n & c2 e a2 =>
EXIST(d):[d e b & (c1,c2,d) e add]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add &
(c1,c2,d2) e add => d1=d2]
=>
ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 249
251 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e b]
&
ALL(c1):ALL(c2):[c1 e n & c2 e n =>
EXIST(d):[d e b & (c1,c2,d) e add]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add &
(c1,c2,d2) e add => d1=d2]
=>
ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 250
Sufficient: For functionality
of add
252 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
&
ALL(c1):ALL(c2):[c1 e n & c2 e n =>
EXIST(d):[d e n & (c1,c2,d) e add]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add &
(c1,c2,d2) e add => d1=d2]
=>
ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]
U Spec, 251
Prove: ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]
Suppose...
253 (x,y,z) e add
Premise
254 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
255 ALL(c):[(x,y,c) e add
<=>
(x,y,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,c) e d]]
U Spec, 254
256 (x,y,z) e add
<=>
(x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
U Spec, 255
257 [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add]
Iff-And, 256
258 (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Split, 257
259 (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add
Split, 257
260 (x,y,z) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Detach, 258, 253
261 (x,y,z) e n3
Split, 260
262 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z) e d]
Split, 260
263 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
264 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 263
265 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 264
266 [(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, 265
267 (x,y,z) e n3 => x e n & y e n & z e n
Split, 266
268 x e n & y e n & z e n => (x,y,z) e n3
Split, 266
269 x e n & y e n & z e n
Detach, 267, 261
As Required: Functionality,
Part 1
270 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]
4 Conclusion, 253
Prove: ALL(a):[a e n =>
EXIST(b):[b e n & (a,0,b) e add]]
Suppose...
271 x e n
Premise
272 x e n => (x,0,x) e add
U Spec, 52
273 (x,0,x) e add
Detach, 272, 271
274 x e n & (x,0,x) e add
Join, 271, 273
275 EXIST(b):[b e n & (x,0,b) e add]
E Gen, 274
As Required:
276 ALL(a):[a e n => EXIST(b):[b e n & (a,0,b) e add]]
4 Conclusion, 271
Prove: ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e add]]]
Suppose...
277 x e n
Premise
278 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]]
Subset, 1
279 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]
E Spec, 278
Prove: p1
*********
280 Set(p1)
Split, 279
281 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]
Split, 279
Apply PMI axiom
282 Set(p1) & ALL(b):[b e p1 => b e n]
=>
[0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=>
ALL(b):[b e n => b e p1]]
U Spec, 6
Prove: ALL(b):[b e p1 => b e n]
Suppose...
283 y e p1
Premise
284 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 281
285 [y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 284
286 y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]
Split, 285
287 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 285
288 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 286, 283
289 y e n
Split, 288
As Required:
290 ALL(b):[b e p1 => b e n]
4 Conclusion, 283
291 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 280, 290
Sufficient: ALL(b):[b e n => b e p1]
292 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=>
ALL(b):[b e n => b e p1]
Detach, 282, 291
293 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e add]
U Spec, 281
294 [0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e add]]
&
[0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1]
Iff-And, 293
295 0 e p1 => 0 e n &
EXIST(c):[c e n & (x,0,c) e add]
Split, 294
Sufficient: 0 e p1
296 0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1
Split, 294
297 x e n => EXIST(b):[b e n & (x,0,b) e add]
U Spec, 276
298 EXIST(b):[b e n & (x,0,b) e add]
Detach, 297, 277
299 0 e n & EXIST(b):[b e n & (x,0,b) e add]
Join, 2, 298
As Required:
300 0 e p1
Detach, 296, 299
Prove: ALL(b):[b e p1 =>
next(b) e p1]
Suppose...
301 y e p1
Premise
302 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 281
303 [y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 302
304 y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]
Split, 303
305 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 303
306 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 304, 301
307 y e n
Split, 306
308 EXIST(c):[c e n & (x,y,c) e add]
Split, 306
309 z e n & (x,y,z) e add
E Spec, 308
310 z e n
Split, 309
311 (x,y,z) e add
Split, 309
312 next(y) e p1 <=> next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]
U Spec, 281
313 [next(y) e p1 => next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]]
&
[next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add] => next(y) e p1]
Iff-And, 312
314 next(y) e p1 => next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]
Split, 313
Sufficient: next(y) e p1
315 next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add] => next(y) e p1
Split, 313
316 y e n => next(y) e n
U Spec, 3
317 next(y) e n
Detach, 316, 307
318 ALL(b):ALL(c):[x e n & b e n & c e n
=>
[(x,b,c) e add => (x,next(b),next(c)) e add]]
U Spec, 100
319 ALL(c):[x e n & y e n & c e n
=>
[(x,y,c) e add => (x,next(y),next(c)) e add]]
U Spec, 318
320 x e n & y e n & z e n
=>
[(x,y,z) e add => (x,next(y),next(z)) e add]
U Spec, 319
321 x e n & y e n
Join, 277, 307
322 x e n & y e n & z e n
Join, 321, 310
323 (x,y,z) e add => (x,next(y),next(z)) e add
Detach, 320, 322
324 (x,next(y),next(z)) e add
Detach, 323, 311
325 z e n => next(z) e n
U Spec, 3
326 next(z) e n
Detach, 325, 310
327 next(z) e n & (x,next(y),next(z)) e add
Join, 326, 324
328 EXIST(c):[c e n & (x,next(y),c) e add]
E Gen, 327
329 next(y) e n
&
EXIST(c):[c e n & (x,next(y),c) e add]
Join, 317, 328
330 next(y) e p1
Detach, 315, 329
As Required:
331 ALL(b):[b e p1 => next(b) e p1]
4 Conclusion, 301
332 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
Join, 300, 331
As Required:
333 ALL(b):[b e n => b e p1]
Detach, 292, 332
Prove: ALL(b):[b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
Suppose...
334 y e n
Premise
335 y e n => y e p1
U Spec, 333
336 y e p1
Detach, 335, 334
337 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 281
338 [y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 337
339 y e p1 => y e n &
EXIST(c):[c e n & (x,y,c) e add]
Split, 338
340 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 338
341 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 339, 336
342 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 339, 336
343 y e n
Split, 342
344 EXIST(c):[c e n & (x,y,c) e add]
Split, 342
As Required:
345 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]
4 Conclusion, 334
As Required:
346 ALL(a):[a e n
=>
ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e add]]]
4 Conclusion, 277
Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]
Suppose...
347 x e n & y e n
Premise
348 x e n
Split, 347
349 y e n
Split, 347
350 x e n
=>
ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]
U Spec, 346
351 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]
Detach, 350, 348
352 y e n => EXIST(c):[c e n & (x,y,c) e add]
U Spec, 351
353 EXIST(c):[c e n & (x,y,c) e add]
Detach, 352, 349
As Required: Functionality,
Part 2
354 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]
4 Conclusion, 347
************************************************
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 add &
(a,b,c2) e add => c1=c2]]]]
Suppose...
355 x e n
Premise
356 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 add & (x,b,c2) e add => c1=c2]]]]
Subset, 1
357 Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]
E Spec, 356
Define: p2
**********
358 Set(p2)
Split, 357
359 ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]
Split, 357
360 Set(p2) & ALL(b):[b e p2 => b e n]
=>
[0 e p2 & ALL(b):[b e p2 => next(b) e p2]
=>
ALL(b):[b e n => b e p2]]
U Spec, 6
Prove: ALL(b):[b e p2 => b e n]
Suppose...
361 y e p2
Premise
362 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
U Spec, 359
363 [y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]
&
[y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]
Iff-And, 362
364 y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Split, 363
365 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2
Split, 363
366 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Detach, 364, 361
367 y e n
Split, 366
As Required:
368 ALL(b):[b e p2 => b e n]
4 Conclusion, 361
369 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 358, 368
Sufficient: ALL(b):[b e n => b e p2]
370 0 e p2 & ALL(b):[b e p2 => next(b) e p2]
=>
ALL(b):[b e n => b e p2]
Detach, 360, 369
371 0 e p2 <=> 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]
U Spec, 359
372 [0 e p2 => 0 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]]
&
[0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]] => 0 e p2]
Iff-And, 371
373 0 e p2 => 0 e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]
Split, 372
Sufficient: 0 e p2
374 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]] => 0 e p2
Split, 372
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,0,c1)
e add & (x,0,c2) e add =>
c1=c2]]
Suppose...
375 z1 e n & z2 e n
Premise
376 z1 e n
Split, 375
377 z2 e n
Split, 375
Prove: (x,0,z1) e add &
(x,0,z2) e add => z1=z2
Suppose...
378 (x,0,z1) e add & (x,0,z2) e add
Premise
379 (x,0,z1) e add
Split, 378
380 (x,0,z2) e add
Split, 378
Apply previous result
381 x e n => ALL(b):[b e n => [(x,0,b) e add => b=x]]
U Spec, 247
382 ALL(b):[b e n => [(x,0,b) e add => b=x]]
Detach, 381, 355
383 z1 e n => [(x,0,z1) e add => z1=x]
U Spec, 382
384 (x,0,z1) e add => z1=x
Detach, 383, 376
385 z1=x
Detach, 384, 379
386 z2 e n => [(x,0,z2) e add => z2=x]
U Spec, 382
387 (x,0,z2) e add => z2=x
Detach, 386, 377
388 z2=x
Detach, 387, 380
389 z1=z2
Substitute, 388,
385
As Required:
390 (x,0,z1) e add & (x,0,z2) e add => z1=z2
4 Conclusion, 378
As Required:
391 ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,0,c1) e add & (x,0,c2) e add => c1=c2]]
4 Conclusion, 375
392 0 e n
&
ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,0,c1) e add & (x,0,c2) e add => c1=c2]]
Join, 2, 391
As Required:
393 0 e p2
Detach, 374, 392
Prove: ALL(b):[b e p2 =>
next(b) e p2]
Suppose...
394 y e p2
Premise
395 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
U Spec, 359
396 [y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]
&
[y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]
Iff-And, 395
397 y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Split, 396
398 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2
Split, 396
399 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Detach, 397, 394
400 y e n
Split, 399
******************************************************
x+y has a unique value
401 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Split, 399
Apply definition of p2
402 next(y) e p2 <=> next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]
U Spec, 359
403 [next(y) e p2 => next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]]
&
[next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]] => next(y) e p2]
Iff-And, 402
404 next(y) e p2 => next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]
Split, 403
Sufficient: next(y) e p2 ***************************
405 next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]] => next(y) e p2
Split, 403
406 y e n => next(y) e n
U Spec, 3
As Required:
407 next(y) e n
Detach, 406, 400
Apply functionality of add, part 2 *********************************
408 ALL(b):[x e n & b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
U Spec, 354
409 x e n & y e n =>
EXIST(c):[c e n & (x,y,c) e add]
U Spec, 408
410 x e n & y e n
Join, 355, 400
411 EXIST(c):[c e n & (x,y,c) e add]
Detach, 409, 410
412 z e n & (x,y,z) e add
E Spec, 411
Define: z x+y=z
413 z e n
Split, 412
414 (x,y,z) e add
Split, 412
Prove: ALL(c):[c e n => [(x,y,c) e add =>
z=c]]
Suppose...
415 z' e n
Premise
416 ALL(c2):[z e n & c2 e n => [(x,y,z) e add & (x,y,c2) e add => z=c2]]
U Spec, 401
417 z e n & z' e n => [(x,y,z) e add & (x,y,z') e add => z=z']
U Spec, 416
418 z e n & z' e n
Join, 413, 415
419 (x,y,z) e add & (x,y,z') e add => z=z'
Detach, 417, 418
Prove: (x,y,z') e add => z=z'
Suppose...
420 (x,y,z') e add
Premise
421 (x,y,z) e add & (x,y,z') e add
Join, 414, 420
422 z=z'
Detach, 419, 421
As Required:
423 (x,y,z') e add => z=z'
4 Conclusion, 420
As Required:
*************************************************
424 ALL(c):[c e n => [(x,y,c) e add => z=c]]
4 Conclusion, 415
Prove: ALL(c'):[c' e n => [(x,next(y),c') e add =>
c'=next(z)]]
Suppose...
425 z' e n
Premise
Prove: (x,next(y),z') e add & ~z'=next(z)
Suppose to the contrary...
426 (x,next(y),z') e add & ~z'=next(z)
Premise
427 (x,next(y),z') e add
Split, 426
428 ~z'=next(z)
Split, 426
429 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
430 ALL(c):[(x,next(y),c) e add
<=>
(x,next(y),c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),c) e d]]
U Spec, 429
431 (x,next(y),z') e add
<=>
(x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d]
U Spec, 430
432 [(x,next(y),z') e add => (x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d]]
&
[(x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d] => (x,next(y),z') e add]
Iff-And, 431
433 (x,next(y),z') e add => (x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d]
Split, 432
434 (x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d] => (x,next(y),z') e add
Split, 432
435 ~[(x,next(y),z') e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d]] => ~(x,next(y),z') e add
Contra, 433
436 ~~[~(x,next(y),z') e n3 | ~ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d]] => ~(x,next(y),z') e add
DeMorgan, 435
437 ~(x,next(y),z') e n3 | ~ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d] => ~(x,next(y),z') e add
Rem DNeg, 436
438 ~(x,next(y),z') e n3 | ~~EXIST(d):~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d] => ~(x,next(y),z') e add
Quant, 437
439 ~(x,next(y),z') e n3 | EXIST(d):~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,next(y),z') e d] => ~(x,next(y),z') e add
Rem DNeg, 438
440 ~(x,next(y),z') e n3 | EXIST(d):~~[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,next(y),z') e d] => ~(x,next(y),z') e add
Imply-And, 439
Sufficient: ~(x,next(y),z')
e add (to obtain
contradiction)
Use d=q as defined below
441 ~(x,next(y),z') e n3 | EXIST(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,next(y),z') e d] => ~(x,next(y),z') e add
Rem DNeg, 440
442 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e add & ~[a=x & b=next(y) & c=z']]]
Subset, 25
443 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e add & ~[a=x & b=next(y) & c=z']]
E Spec, 442
Define: q
444 Set''(q)
Split, 443
445 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=>
(a,b,c) e add & ~[a=x & b=next(y) & c=z']]
Split, 443
446 q e pn3 <=> Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
U Spec, 22
447 [q e pn3 => Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]]
&
[Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]
Iff-And, 446
448 q e pn3 => Set''(q) &
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
Split, 447
449 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 447
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Suppose...
450 (t,u,v) e q
Premise
451 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=next(y) & c=z']]
U Spec, 445
452 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e add & ~[t=x & u=next(y) & c=z']]
U Spec, 451
453 (t,u,v) e q
<=>
(t,u,v) e add & ~[t=x & u=next(y) & v=z']
U Spec, 452
454 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']]
&
[(t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q]
Iff-And, 453
455 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']
Split, 454
456 (t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q
Split, 454
457 (t,u,v) e add & ~[t=x & u=next(y) & v=z']
Detach, 455, 450
458 (t,u,v) e add
Split, 457
459 ~[t=x & u=next(y) & v=z']
Split, 457
460 ALL(b):ALL(c):[(t,b,c) e add
<=>
(t,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,b,c) e d]]
U Spec, 26
461 ALL(c):[(t,u,c) e add
<=>
(t,u,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,c) e d]]
U Spec, 460
462 (t,u,v) e add
<=>
(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
U Spec, 461
463 [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add]
Iff-And, 462
464 (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 463
465 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add
Split, 463
466 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Detach, 464, 458
467 (t,u,v) e n3
Split, 466
As Required:
468 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
4 Conclusion, 450
469 Set''(q)
&
ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q =>
(d1,d2,d3) e n3]
Join, 444, 468
As Required:
470 q e pn3
Detach, 449, 469
Prove: ALL(e):[e e n =>
(e,0,e) e q]
Suppose...
471 t e n
Premise
472 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=next(y) & c=z']]
U Spec, 445
473 ALL(c):[(t,0,c) e q
<=>
(t,0,c) e add & ~[t=x & 0=next(y) & c=z']]
U Spec, 472
474 (t,0,t) e q
<=>
(t,0,t) e add & ~[t=x & 0=next(y) & t=z']
U Spec, 473
475 [(t,0,t) e q => (t,0,t) e add & ~[t=x & 0=next(y) & t=z']]
&
[(t,0,t) e add & ~[t=x & 0=next(y) & t=z'] => (t,0,t) e q]
Iff-And, 474
476 (t,0,t) e q => (t,0,t) e add & ~[t=x & 0=next(y) & t=z']
Split, 475
477 (t,0,t) e add & ~[t=x & 0=next(y) & t=z'] => (t,0,t) e q
Split, 475
478 t e n => (t,0,t) e add
U Spec, 52
479 (t,0,t) e add
Detach, 478, 471
Prove: t=x & 0=next(y) & t=z'
Suppose to the contrary...
480 t=x & 0=next(y) & t=z'
Premise
481 t=x
Split, 480
482 0=next(y)
Split, 480
483 t=z'
Split, 480
484 y e n => ~next(y)=0
U Spec, 5
485 ~next(y)=0
Detach, 484, 400
486 ~0=next(y)
Sym, 485
Obtain the contradiction...
487 0=next(y) & ~0=next(y)
Join, 482, 486
As Required:
488 ~[t=x & 0=next(y) & t=z']
4 Conclusion, 480
489 (t,0,t) e add & ~[t=x & 0=next(y) & t=z']
Join, 479, 488
490 (t,0,t) e q
Detach, 477, 489
As Required:
491 ALL(e):[e e n => (e,0,e) e q]
4 Conclusion, 471
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Suppose...
492 (t,u,v) e q
Premise
493 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=next(y) & c=z']]
U Spec, 445
494 ALL(c):[(t,u,c) e q
<=>
(t,u,c) e add & ~[t=x & u=next(y) & c=z']]
U Spec, 493
495 (t,u,v) e q
<=>
(t,u,v) e add & ~[t=x & u=next(y) & v=z']
U Spec, 494
496 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']]
&
[(t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q]
Iff-And, 495
497 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']
Split, 496
498 (t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q
Split, 496
499 (t,u,v) e add & ~[t=x & u=next(y) & v=z']
Detach, 497, 492
500 (t,u,v) e add
Split, 499
501 ~[t=x & u=next(y) & v=z']
Split, 499
502 ALL(b):ALL(c):[(t,b,c) e add
<=>
(t,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,b,c) e d]]
U Spec, 26
503 ALL(c):[(t,u,c) e add
<=>
(t,u,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,c) e d]]
U Spec, 502
504 (t,u,v) e add
<=>
(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
U Spec, 503
505 [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]]
&
[(t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=> (t,u,v) e d] => (t,u,v) e add]
Iff-And, 504
506 (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 505
507 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add
Split, 505
508 (t,u,v) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Detach, 506, 500
509 (t,u,v) e n3
Split, 508
510 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 16
511 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 510
512 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 511
513 [(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, 512
514 (t,u,v) e n3 => t e n & u e n & v e n
Split, 513
515 t e n & u e n & v e n => (t,u,v) e n3
Split, 513
516 t e n & u e n & v e n
Detach, 514, 509
517 t e n
Split, 516
518 u e n
Split, 516
519 v e n
Split, 516
520 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(t,u,v) e d]
Split, 508
521 ALL(b):ALL(c):[(t,b,c) e q
<=>
(t,b,c) e add & ~[t=x & b=next(y) & c=z']]
U Spec, 445
522 ALL(c):[(t,next(u),c) e q
<=>
(t,next(u),c) e add & ~[t=x & next(u)=next(y) & c=z']]
U Spec, 521
523 (t,next(u),next(v)) e q
<=> (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']
U Spec, 522
524 [(t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']]
&
[(t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) e q]
Iff-And, 523
525 (t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']
Split, 524
Sufficient: (t,next(u),next(v))
e q
526 (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) e q
Split, 524
527 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e add => (t,next(b),next(c)) e add]]
U Spec, 100
528 ALL(c):[t e n & u e n & c e n
=> [(t,u,c) e add => (t,next(u),next(c)) e add]]
U Spec, 527
529 t e n & u e n & v e n
=>
[(t,u,v) e add => (t,next(u),next(v)) e add]
U Spec, 528
530 (t,u,v) e add => (t,next(u),next(v)) e add
Detach, 529, 516
531 (t,next(u),next(v)) e add
Detach, 530, 500
Prove: t=x & next(u)=next(y) &
next(v)=z'
Suppose to the contrary...
532 t=x & next(u)=next(y) & next(v)=z'
Premise
533 t=x
Split, 532
534 next(u)=next(y)
Split, 532
535 next(v)=z'
Split, 532
536 ALL(b):[u e n & b e n => [next(u)=next(b) => u=b]]
U Spec, 4
537 u e n & y e n => [next(u)=next(y) => u=y]
U Spec, 536
538 u e n & y e n
Join, 518, 400
539 next(u)=next(y) => u=y
Detach, 537, 538
540 u=y
Detach, 539, 534
541 (x,u,v) e add
Substitute, 533,
500
542 (x,y,v) e add
Substitute, 540,
541
543 v e n => [(x,y,v) e add => z=v]
U Spec, 424
544 (x,y,v) e add => z=v
Detach, 543, 519
545 z=v
Detach, 544, 542
546 next(z)=z'
Substitute, 545,
535
547 z'=next(z)
Sym, 546
Obtain the contradiction...
548 ~z'=next(z) & z'=next(z)
Join, 428, 547
As Required:
549 ~[t=x & next(u)=next(y) & next(v)=z']
4 Conclusion, 532
550 (t,next(u),next(v)) e add
&
~[t=x & next(u)=next(y) & next(v)=z']
Join, 531, 549
551 (t,next(u),next(v)) e q
Detach, 526, 550
As Required:
552 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
4 Conclusion, 492
553 ALL(b):ALL(c):[(x,b,c) e q
<=>
(x,b,c) e add & ~[x=x & b=next(y) & c=z']]
U Spec, 445
554 ALL(c):[(x,next(y),c) e q
<=>
(x,next(y),c) e add & ~[x=x & next(y)=next(y) & c=z']]
U Spec, 553
555 (x,next(y),z') e q
<=>
(x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']
U Spec, 554
556 [(x,next(y),z') e q => (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']]
&
[(x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') e q]
Iff-And, 555
557 (x,next(y),z') e q => (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']
Split, 556
558 (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') e q
Split, 556
559 ~[(x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') e q
Contra, 557
560 ~~[~(x,next(y),z') e add | ~~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') e q
DeMorgan, 559
561 ~(x,next(y),z') e add | ~~[x=x & next(y)=next(y) & z'=z'] => ~(x,next(y),z') e q
Rem DNeg, 560
562 ~(x,next(y),z') e add | x=x & next(y)=next(y) & z'=z' => ~(x,next(y),z') e q
Rem DNeg, 561
563 x=x
Reflex
564 next(y)=next(y)
Reflex
565 z'=z'
Reflex
566 x=x & next(y)=next(y)
Join, 563, 564
567 x=x & next(y)=next(y) & z'=z'
Join, 566, 565
568 ~(x,next(y),z') e add | x=x & next(y)=next(y) & z'=z'
Arb Or, 567
As Required:
569 ~(x,next(y),z') e q
Detach, 562, 568
570 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
Join, 470, 491
571 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
Join, 570, 552
572 q e pn3 & ALL(e):[e e n => (e,0,e) e q]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]
&
~(x,next(y),z') e q
Join, 571, 569
573 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
&
~(x,next(y),z') e d]
E Gen, 572
574 ~(x,next(y),z') e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
&
~(x,next(y),z') e d]
Arb Or, 573
575 ~(x,next(y),z') e add
Detach, 441, 574
Obtain the contradiction...
576 (x,next(y),z') e add & ~(x,next(y),z') e add
Join, 427, 575
As Required:
577 ~[(x,next(y),z') e add & ~z'=next(z)]
4 Conclusion, 426
578 ~~[(x,next(y),z') e add => ~~z'=next(z)]
Imply-And, 577
579 (x,next(y),z') e add => ~~z'=next(z)
Rem DNeg, 578
580 (x,next(y),z') e add => z'=next(z)
Rem DNeg, 579
As Required:
581 ALL(c'):[c' e n => [(x,next(y),c') e add => c'=next(z)]]
4 Conclusion, 425
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,next(y),c1) e add & (x,next(y),c2) e add =>
c1=c2]]
Suppose...
582 z1 e n & z2 e n
Premise
583 z1 e n
Split, 582
584 z2 e n
Split, 582
Prove: (x,next(y),z1) e add & (x,next(y),z2) e add => z1=z2
Suppose...
585 (x,next(y),z1) e add & (x,next(y),z2) e add
Premise
586 (x,next(y),z1) e add
Split, 585
587 (x,next(y),z2) e add
Split, 585
588 z1 e n => [(x,next(y),z1) e add => z1=next(z)]
U Spec, 581
589 (x,next(y),z1) e add => z1=next(z)
Detach, 588, 583
590 z1=next(z)
Detach, 589, 586
591 z2 e n => [(x,next(y),z2) e add => z2=next(z)]
U Spec, 581
592 (x,next(y),z2) e add => z2=next(z)
Detach, 591, 584
593 z2=next(z)
Detach, 592, 587
594 z1=z2
Substitute, 593,
590
As Required:
595 (x,next(y),z1) e add & (x,next(y),z2) e add => z1=z2
4 Conclusion, 585
As Required:
596 ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]
4 Conclusion, 582
597 next(y) e n
&
ALL(c1):ALL(c2):[c1 e n & c2 e n
=>
[(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]
Join, 407, 596
598 next(y) e p2
Detach, 405, 597
As Required:
599 ALL(b):[b e p2 => next(b) e p2]
4 Conclusion, 394
600 0 e p2 & ALL(b):[b e p2 => next(b) e p2]
Join, 393, 599
As Required:
601 ALL(b):[b e n => b e p2]
Detach, 370, 600
Prove: ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add &
(x,b,c2) e add => c1=c2]]]
Suppose...
602 y e n
Premise
603 y e n => y e p2
U Spec, 601
604 y e p2
Detach, 603, 602
605 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
U Spec, 359
606 [y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]
&
[y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]
Iff-And, 605
607 y e p2 => y e n &
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Split, 606
608 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2
Split, 606
609 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Detach, 607, 604
610 y e n
Split, 609
611 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Split, 609
As Required:
612 ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]
4 Conclusion, 602
As Required:
613 ALL(a):[a e n
=>
ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e add & (a,b,c2) e add => c1=c2]]]]
4 Conclusion, 355
Prove: ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add =>
d1=d2]
Suppose...
614 (x,y,z1) e add & (x,y,z2) e add
Premise
615 (x,y,z1) e add
Split, 614
616 (x,y,z2) e add
Split, 614
Apply definition of add
617 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,b,c) e d]]
U Spec, 26
618 ALL(c):[(x,y,c) e add
<=>
(x,y,c) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,c) e d]]
U Spec, 617
619 (x,y,z1) e add
<=>
(x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d]
U Spec, 618
620 [(x,y,z1) e add => (x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d]]
&
[(x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d] => (x,y,z1) e add]
Iff-And, 619
621 (x,y,z1) e add => (x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d]
Split, 620
622 (x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d] => (x,y,z1) e add
Split, 620
623 (x,y,z1) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d]
Detach, 621, 615
624 (x,y,z1) e n3
Split, 623
625 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z1) e d]
Split, 623
Apply definition of n3
626 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
627 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 626
628 (x,y,z1) e n3 <=> x e n & y e n & z1 e n
U Spec, 627
629 [(x,y,z1) e n3 => x e n & y e n & z1 e n]
&
[x e n & y e n & z1 e n => (x,y,z1) e n3]
Iff-And, 628
630 (x,y,z1) e n3 => x e n & y e n & z1 e n
Split, 629
631 x e n & y e n & z1 e n => (x,y,z1) e n3
Split, 629
632 x e n & y e n & z1 e n
Detach, 630, 624
633 x e n
Split, 632
634 y e n
Split, 632
635 z1 e n
Split, 632
Apply definition of add
636 (x,y,z2) e add
<=>
(x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d]
U Spec, 618
637 [(x,y,z2) e add => (x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d]]
&
[(x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d] => (x,y,z2) e add]
Iff-And, 636
638 (x,y,z2) e add => (x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d]
Split, 637
639 (x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d] => (x,y,z2) e add
Split, 637
640 (x,y,z2) e n3 & ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d]
Detach, 638, 616
641 (x,y,z2) e n3
Split, 640
642 ALL(d):[d e pn3
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]
=>
(x,y,z2) e d]
Split, 640
Apply definition of n3
643 (x,y,z2) e n3 <=> x e n & y e n & z2 e n
U Spec, 627
644 [(x,y,z2) e n3 => x e n & y e n & z2 e n]
&
[x e n & y e n & z2 e n => (x,y,z2) e n3]
Iff-And, 643
645 (x,y,z2) e n3 => x e n & y e n & z2 e n
Split, 644
646 x e n & y e n & z2 e n => (x,y,z2) e n3
Split, 644
647 x e n & y e n & z2 e n
Detach, 645, 641
648 x e n
Split, 647
649 y e n
Split, 647
650 z2 e n
Split, 647
651 x e n
=>
ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]
U Spec, 613
652 ALL(b):[b e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]
Detach, 651, 633
653 y e n
=>
ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
U Spec, 652
654 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
Detach, 653, 634
655 ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e add & (x,y,c2) e add => z1=c2]]
U Spec, 654
656 z1 e n & z2 e n => [(x,y,z1) e add & (x,y,z2) e add => z1=z2]
U Spec, 655
657 z1 e n & z2 e n
Join, 635, 650
658 (x,y,z1) e add & (x,y,z2) e add => z1=z2
Detach, 656, 657
659 z1=z2
Detach, 658, 614
As Required: Functionality,
Part 3
660 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
4 Conclusion, 614
661 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]
&
ALL(a):ALL(b):[a e n & b e n =>
EXIST(c):[c e n & (a,b,c) e add]]
Join, 270, 354
662 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]
&
ALL(a):ALL(b):[a e n & b e n =>
EXIST(c):[c e n & (a,b,c) e add]]
&
ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add &
(c1,c2,d2) e add => d1=d2]
Join, 661, 660
As Required: add is a function
663 ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2)
<=> (c1,c2,d) e add]
Detach, 252, 662
664 x e n & y e n
Premise
665 x e n
Split, 664
666 y e n
Split, 664
667 ALL(b):[x e n & b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
U Spec, 354
668 x e n & y e n =>
EXIST(c):[c e n & (x,y,c) e add]
U Spec, 667
669 EXIST(c):[c e n & (x,y,c) e add]
Detach, 668, 664
670 z e n & (x,y,z) e add
E Spec, 669
671 z e n
Split, 670
672 (x,y,z) e add
Split, 670
673 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 663
674 ALL(d):[d=add(x,y) <=> (x,y,d) e add]
U Spec, 673
675 z=add(x,y) <=> (x,y,z) e add
U Spec, 674
676 [z=add(x,y) => (x,y,z) e add]
&
[(x,y,z) e add => z=add(x,y)]
Iff-And, 675
677 z=add(x,y) => (x,y,z) e add
Split, 676
678 (x,y,z) e add => z=add(x,y)
Split, 676
679 z=add(x,y)
Detach, 678, 672
680 add(x,y) e n
Substitute, 679,
671
As Required:
681 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
4 Conclusion, 664
Prove: ALL(a):[a e n =>
add(a,0)=a]
Suppose...
682 x e n
Premise
683 x e n => (x,0,x) e add
U Spec, 52
684 (x,0,x) e add
Detach, 683, 682
685 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 663
686 ALL(d):[d=add(x,0) <=> (x,0,d) e add]
U Spec, 685
687 x=add(x,0) <=> (x,0,x) e add
U Spec, 686
688 [x=add(x,0) => (x,0,x) e add]
&
[(x,0,x) e add => x=add(x,0)]
Iff-And, 687
689 x=add(x,0) => (x,0,x) e add
Split, 688
690 (x,0,x) e add => x=add(x,0)
Split, 688
691 x=add(x,0)
Detach, 690, 684
692 add(x,0)=x
Sym, 691
As Required:
693 ALL(a):[a e n => add(a,0)=a]
4 Conclusion, 682
Prove: ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
Suppose...
694 x e n & y e n
Premise
695 x e n
Split, 694
696 y e n
Split, 694
697 ALL(b):[x e n & b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
U Spec, 354
698 x e n & y e n =>
EXIST(c):[c e n & (x,y,c) e add]
U Spec, 697
699 EXIST(c):[c e n & (x,y,c) e add]
Detach, 698, 694
700 z e n & (x,y,z) e add
E Spec, 699
701 z e n
Split, 700
702 (x,y,z) e add
Split, 700
703 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 663
704 ALL(d):[d=add(x,y) <=> (x,y,d) e add]
U Spec, 703
705 z=add(x,y) <=> (x,y,z) e add
U Spec, 704
706 [z=add(x,y) => (x,y,z) e add]
&
[(x,y,z) e add => z=add(x,y)]
Iff-And, 705
707 z=add(x,y) => (x,y,z) e add
Split, 706
708 (x,y,z) e add => z=add(x,y)
Split, 706
709 z=add(x,y)
Detach, 708, 702
710 ALL(b):ALL(c):[x e n & b e n & c e n
=>
[(x,b,c) e add => (x,next(b),next(c)) e add]]
U Spec, 100
711 ALL(c):[x e n & y e n & c e n
=>
[(x,y,c) e add => (x,next(y),next(c)) e add]]
U Spec, 710
712 x e n & y e n & z e n
=>
[(x,y,z) e add => (x,next(y),next(z)) e add]
U Spec, 711
713 x e n & y e n & z e n
Join, 694, 701
714 (x,y,z) e add => (x,next(y),next(z)) e add
Detach, 712, 713
715 (x,next(y),next(z)) e add
Detach, 714, 702
716 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 663
717 ALL(d):[d=add(x,next(y)) <=> (x,next(y),d) e add]
U Spec, 716
718 next(z)=add(x,next(y)) <=> (x,next(y),next(z)) e add
U Spec, 717
719 [next(z)=add(x,next(y)) => (x,next(y),next(z)) e add]
&
[(x,next(y),next(z)) e add => next(z)=add(x,next(y))]
Iff-And, 718
720 next(z)=add(x,next(y)) => (x,next(y),next(z)) e add
Split, 719
721 (x,next(y),next(z)) e add => next(z)=add(x,next(y))
Split, 719
722 next(z)=add(x,next(y))
Detach, 721, 715
723 next(add(x,y))=add(x,next(y))
Substitute, 709,
722
724 add(x,next(y))=next(add(x,y))
Sym, 723
As Required:
725 ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
4 Conclusion, 694
Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & add(a,b)=c]]
Suppose...
726 x e n & y e n
Premise
727 ALL(b):[x e n & b e n => add(x,b) e n]
U Spec, 681
728 x e n & y e n => add(x,y) e n
U Spec, 727
729 add(x,y) e n
Detach, 728, 726
730 add(x,y)=add(x,y)
Reflex
731 add(x,y) e n & add(x,y)=add(x,y)
Join, 729, 730
732 EXIST(c):[c e n & add(x,y)=c]
E Gen, 731
As Required:
733 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & add(a,b)=c]]
4 Conclusion, 726
Prove: ALL(a):[a e n =>
EXIST(b):[b e n & next(a)=b]]
Suppose...
734 x e n
Premise
735 x e n => next(x) e n
U Spec, 3
736 next(x) e n
Detach, 735, 734
737 next(x)=next(x)
Reflex
738 next(x) e n & next(x)=next(x)
Join, 736, 737
739 EXIST(b):[b e n & next(x)=b]
E Gen, 738
As Required:
740 ALL(a):[a e n => EXIST(b):[b e n & next(a)=b]]
4 Conclusion, 734
Prove: add(1,1)=2
Apply previous result.
741 0 e n => EXIST(b):[b e n & next(0)=b]
U Spec, 740
742 EXIST(b):[b e n & next(0)=b]
Detach, 741, 2
743 1 e n & next(0)=1
E Spec, 742
Define: 1
744 1 e n
Split, 743
745 next(0)=1
Split, 743
746 1 e n => EXIST(b):[b e n & next(1)=b]
U Spec, 740
747 EXIST(b):[b e n & next(1)=b]
Detach, 746, 744
748 2 e n & next(1)=2
E Spec, 747
Define: 2
749 2 e n
Split, 748
750 next(1)=2
Split, 748
Apply previous result
751 1 e n => add(1,0)=1
U Spec, 693
752 add(1,0)=1
Detach, 751, 744
753 add(1,0)=1
Detach, 751, 744
754 ALL(b):[1 e n & b e n => add(1,next(b))=next(add(1,b))]
U Spec, 725
755 1 e n & 0 e n => add(1,next(0))=next(add(1,0))
U Spec, 754
756 1 e n & 0 e n
Join, 744, 2
757 add(1,next(0))=next(add(1,0))
Detach, 755, 756
758 add(1,1)=next(add(1,0))
Substitute, 745,
757
759 add(1,1)=next(1)
Substitute, 753,
758
As Required:
760 add(1,1)=2
Substitute, 750,
759