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