THEOREM
*******
Given the following axioms for a successor relation on a finite set n (lines 1 -8), we construct an add relation on n and prove:
ALL(a):[a e n => (a,0,a) e add] (Lines 85 - 111
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~b=max & ~c=max (Lines 112 - 165)
=> [(a,b,c) e add => (a,s(b),s(c)) e add]]
ALL(a):ALL(b):ALL(c):ALL(d):[a e n & b e n & c e n & d e n (Lines 223 - End)
=> [(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 & ~b=max & ~c=max
=> [a+b=c => a+s(b)=s(c)]]
Dan Christensen
Originally posted: 2014-04-12
Last updated: 2014-04-14
This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
THE INTUITION
*************
Intuitively, 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. Thus, the successor relation s is a partial function on n.
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
0 has no predecessor
6 ALL(a):[a e n & ~a=max => ~s(a)=0]
Axiom
Uniqueness of predecessors
7 ALL(a):ALL(b):[a e n & b e n & ~a=max & ~b=max => [s(a)=s(b) => a=b]]
Axiom
Finite Induction
8 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a & ~b=max => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
Prove: ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & s(b)=a]]]
Apply Subset Axiom
9 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [~a=0 => EXIST(b):[b e n & s(b)=a]]]]
Subset, 1
10 Set(p1) & ALL(a):[a e p1 <=> a e n & [~a=0 => EXIST(b):[b e n & s(b)=a]]]
E Spec, 9
Define: p1
11 Set(p1)
Split, 10
12 ALL(a):[a e p1 <=> a e n & [~a=0 => EXIST(b):[b e n & s(b)=a]]]
Split, 10
13 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 & ~b=max => s(b) e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 8
14 x e p1
Premise
15 x e p1 <=> x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
U Spec, 12
16 [x e p1 => 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 p1]
Iff-And, 15
17 x e p1 => x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Split, 16
18 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]] => x e p1
Split, 16
19 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Detach, 17, 14
20 x e n
Split, 19
21 ALL(b):[b e p1 => b e n]
4 Conclusion, 14
22 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 11, 21
Sufficient: ALL(b):[b e n => b e p1]
23 0 e p1 & ALL(b):[b e p1 & ~b=max => s(b) e p1]
=> ALL(b):[b e n => b e p1]
Detach, 13, 22
Base Case
Prove: ALL(b):[b e p1 & ~b=max => s(b) e p1]
Apply definition of p1
24 0 e p1 <=> 0 e n & [~0=0 => EXIST(b):[b e n & s(b)=0]]
U Spec, 12
25 [0 e p1 => 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 p1]
Iff-And, 24
26 0 e p1 => 0 e n & [~0=0 => EXIST(b):[b e n & s(b)=0]]
Split, 25
Sufficient: 0 e p1
27 0 e n & [~0=0 => EXIST(b):[b e n & s(b)=0]] => 0 e p1
Split, 25
28 0=0
Reflex
29 ~0=0 => EXIST(b):[b e n & s(b)=0]
Arb Cons, 28
30 0 e n & [~0=0 => EXIST(b):[b e n & s(b)=0]]
Join, 2, 29
As Required:
31 0 e p1
Detach, 27, 30
Inductive Step
Prove: ALL(b):[b e p1 & ~b=max => s(b) e p1]
Suppose...
32 x e p1 & ~x=max
Premise
33 x e p1
Split, 32
34 ~x=max
Split, 32
35 x e p1 <=> x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
U Spec, 12
36 [x e p1 => 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 p1]
Iff-And, 35
37 x e p1 => x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Split, 36
38 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]] => x e p1
Split, 36
39 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Detach, 37, 33
40 x e n
Split, 39
41 ~x=0 => EXIST(b):[b e n & s(b)=x]
Split, 39
42 s(x) e p1 <=> s(x) e n & [~s(x)=0 => EXIST(b):[b e n & s(b)=s(x)]]
U Spec, 12
43 [s(x) e p1 => 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 p1]
Iff-And, 42
44 s(x) e p1 => s(x) e n & [~s(x)=0 => EXIST(b):[b e n & s(b)=s(x)]]
Split, 43
45 s(x) e n & [~s(x)=0 => EXIST(b):[b e n & s(b)=s(x)]] => s(x) e p1
Split, 43
46 s(x) e n & [~~s(x)=0 | EXIST(b):[b e n & s(b)=s(x)]] => s(x) e p1
Imply-Or, 45
Sufficient: s(x) e p
47 s(x) e n & [s(x)=0 | EXIST(b):[b e n & s(b)=s(x)]] => s(x) e p1
Rem DNeg, 46
48 x e n & ~x=max => s(x) e n
U Spec, 5
49 x e n & ~x=max
Join, 40, 34
50 s(x) e n
Detach, 48, 49
51 s(x)=s(x)
Reflex
52 x e n & s(x)=s(x)
Join, 40, 51
53 EXIST(b):[b e n & s(b)=s(x)]
E Gen, 52
54 s(x)=0 | EXIST(b):[b e n & s(b)=s(x)]
Arb Or, 53
55 s(x) e n & [s(x)=0 | EXIST(b):[b e n & s(b)=s(x)]]
Join, 50, 54
56 s(x) e p1
Detach, 47, 55
As Required:
57 ALL(b):[b e p1 & ~b=max => s(b) e p1]
4 Conclusion, 32
58 0 e p1 & ALL(b):[b e p1 & ~b=max => s(b) e p1]
Join, 31, 57
As Required:
59 ALL(b):[b e n => b e p1]
Detach, 23, 58
Prove: ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & s(b)=a]]]
Suppose...
60 x e n
Premise
61 x e n => x e p1
U Spec, 59
62 x e p1
Detach, 61, 60
63 x e p1 <=> x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
U Spec, 12
64 [x e p1 => 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 p1]
Iff-And, 63
65 x e p1 => x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Split, 64
66 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]] => x e p1
Split, 64
67 x e n & [~x=0 => EXIST(b):[b e n & s(b)=x]]
Detach, 65, 62
68 x e n
Split, 67
69 ~x=0 => EXIST(b):[b e n & s(b)=x]
Split, 67
Lemma 1
*******
70 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & s(b)=a]]]
4 Conclusion, 60
71 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
72 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, 71
73 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, 72
74 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, 73
75 Set(n) & Set(n)
Join, 1, 1
76 Set(n) & Set(n) & Set(n)
Join, 75, 1
77 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, 74, 76
78 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 77
Define: n3
**********
79 Set''(n3)
Split, 78
80 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 78
81 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]]
Subset, 79
82 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
E Spec, 81
Define: add
***********
83 Set''(add)
Split, 82
84 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
Split, 82
Prove: ALL(a):[a e n => (a,0,a) e add]
Suppose...
85 x e n
Premise
86 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
87 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,c) e d]]
U Spec, 86
88 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d]
U Spec, 87
89 [(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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d] => (x,0,x) e add]
Iff-And, 88
90 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d]
Split, 89
Sufficient: (x,0,x) e add
91 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d] => (x,0,x) e add
Split, 89
92 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 80
93 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 92
94 (x,0,x) e n3 <=> x e n & 0 e n & x e n
U Spec, 93
95 [(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, 94
96 (x,0,x) e n3 => x e n & 0 e n & x e n
Split, 95
97 x e n & 0 e n & x e n => (x,0,x) e n3
Split, 95
98 x e n & 0 e n
Join, 85, 2
99 x e n & 0 e n & x e n
Join, 98, 85
100 (x,0,x) e n3
Detach, 97, 99
Define: 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d]
Suppose...
101 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
Premise
102 Set''(d)
Split, 101
103 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 101
104 ALL(e):[e e n => (e,0,e) e d]
Split, 101
105 ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
Split, 101
106 x e n => (x,0,x) e d
U Spec, 104
107 (x,0,x) e d
Detach, 106, 85
As Required:
108 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d]
4 Conclusion, 101
109 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,0,x) e d]
Join, 100, 108
110 (x,0,x) e add
Detach, 91, 109
As Required:
111 ALL(a):[a e n => (a,0,a) e add]
4 Conclusion, 85
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~b=max & ~c=max
=> [(a,b,c) e add => (a,s(b),s(c)) e add]]
Suppose...
112 x e n & y e n & z e n & ~y=max & ~z=max
Premise
113 x e n
Split, 112
114 y e n
Split, 112
115 z e n
Split, 112
116 ~y=max
Split, 112
117 ~z=max
Split, 112
118 (x,y,z) e add
Premise
119 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
120 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,c) e d]]
U Spec, 119
121 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
U Spec, 120
122 [(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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 121
123 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 122
124 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add
Split, 122
125 (x,y,z) e n3 & ALL(d):[Set''(d)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Detach, 123, 118
126 (x,y,z) e n3
Split, 125
127 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 125
128 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
129 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,s(y),c) e d]]
U Spec, 128
130 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,s(y),s(z)) e d]
U Spec, 129
131 [(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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(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, 130
132 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,s(y),s(z)) e d]
Split, 131
Sufficient:
133 (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 & ~f=max & ~g=max => [(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, 131
134 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 80
135 ALL(c3):[(x,s(y),c3) e n3 <=> x e n & s(y) e n & c3 e n]
U Spec, 134
136 (x,s(y),s(z)) e n3 <=> x e n & s(y) e n & s(z) e n
U Spec, 135
137 [(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, 136
138 (x,s(y),s(z)) e n3 => x e n & s(y) e n & s(z) e n
Split, 137
139 x e n & s(y) e n & s(z) e n => (x,s(y),s(z)) e n3
Split, 137
140 y e n & ~y=max => s(y) e n
U Spec, 5
141 y e n & ~y=max
Join, 114, 116
142 s(y) e n
Detach, 140, 141
143 z e n & ~z=max => s(z) e n
U Spec, 5
144 z e n & ~z=max
Join, 115, 117
145 s(z) e n
Detach, 143, 144
146 x e n & s(y) e n
Join, 113, 142
147 x e n & s(y) e n & s(z) e n
Join, 146, 145
148 (x,s(y),s(z)) e n3
Detach, 139, 147
149 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
Premise
150 Set''(d)
Split, 149
151 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 149
152 ALL(e):[e e n => (e,0,e) e d]
Split, 149
153 ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
Split, 149
154 ALL(f):ALL(g):[x e n & f e n & g e n & ~f=max & ~g=max => [(x,f,g) e d => (x,s(f),s(g)) e d]]
U Spec, 153
155 ALL(g):[x e n & y e n & g e n & ~y=max & ~g=max => [(x,y,g) e d => (x,s(y),s(g)) e d]]
U Spec, 154
156 x e n & y e n & z e n & ~y=max & ~z=max => [(x,y,z) e d => (x,s(y),s(z)) e d]
U Spec, 155
157 (x,y,z) e d => (x,s(y),s(z)) e d
Detach, 156, 112
158 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d
U Spec, 127
159 (x,y,z) e d
Detach, 158, 149
160 (x,s(y),s(z)) e d
Detach, 157, 159
161 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,s(y),s(z)) e d]
4 Conclusion, 149
162 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,s(y),s(z)) e d]
Join, 148, 161
163 (x,s(y),s(z)) e add
Detach, 133, 162
164 (x,y,z) e add => (x,s(y),s(z)) e add
4 Conclusion, 118
As Required:
165 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~b=max & ~c=max
=> [(a,b,c) e add => (a,s(b),s(c)) e add]]
4 Conclusion, 112
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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]
=> (a,b,c) e add]
Suppose...
166 x e n & y e n & z 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Premise
167 x e n
Split, 166
168 y e n
Split, 166
169 z e n
Split, 166
170 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 166
171 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
172 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,c) e d]]
U Spec, 171
173 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
U Spec, 172
174 [(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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 173
175 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 174
176 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add
Split, 174
177 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 80
178 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 177
179 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 178
180 [(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, 179
181 (x,y,z) e n3 => x e n & y e n & z e n
Split, 180
182 x e n & y e n & z e n => (x,y,z) e n3
Split, 180
183 x e n & y e n
Join, 167, 168
184 x e n & y e n & z e n
Join, 183, 169
185 (x,y,z) e n3
Detach, 182, 184
186 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Join, 185, 170
187 (x,y,z) e add
Detach, 176, 186
Sufficient for (a,b,c) e add
188 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 & ~f=max & ~g=max => [(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):[(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
Suppose...
189 (x,y,z) e add
Premise
190 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
191 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,c) e d]]
U Spec, 190
192 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) 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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 193
195 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add
Split, 193
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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Detach, 194, 189
197 (x,y,z) e n3
Split, 196
198 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 196
Necessary for (a,b,c) e add
199 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
4 Conclusion, 189
200 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Contra, 199
201 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Quant, 200
202 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Rem DNeg, 201
203 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(a,b,c) e d] => ~(a,b,c) e add]
Imply-And, 202
Sufficient for ~(a,b,c) e add
204 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(a,b,c) e d] => ~(a,b,c) e add]
Rem DNeg, 203
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
Suppose...
205 (x,y,z) e add
Premise
206 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,b,c) e d]]
U Spec, 84
207 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,c) e d]]
U Spec, 206
208 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
U Spec, 207
209 [(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 & ~f=max & ~g=max => [(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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 208
210 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 209
211 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d] => (x,y,z) e add
Split, 209
212 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Detach, 210, 205
213 (x,y,z) e n3
Split, 212
214 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (x,y,z) e d]
Split, 212
215 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 80
216 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 215
217 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 216
218 [(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, 217
219 (x,y,z) e n3 => x e n & y e n & z e n
Split, 218
220 x e n & y e n & z e n => (x,y,z) e n3
Split, 218
221 x e n & y e n & z e n
Detach, 219, 213
add is a subset of n3
222 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
4 Conclusion, 205
Prove: ALL(a):ALL(c):[a e n & c e n => [(a,0,c) e add => c=a]]
Suppose...
223 x e n & z e n
Premise
224 x e n
Split, 223
225 z e n
Split, 223
Prove: ~z=x => ~(x,0,z) e add (proof by contrapositive)
Suppose...
226 ~z=x
Premise
227 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(x,b,c) e d] => ~(x,b,c) e add]
U Spec, 204
228 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(x,0,c) e d] => ~(x,0,c) e add]
U Spec, 227
Sufficient: ~(x,0,z) e add
229 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(x,0,z) e d] => ~(x,0,z) e add
U Spec, 228
230 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, 83
231 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, 230
Define: add1 (add without (x,0,z))
************
232 Set''(add1)
Split, 231
233 ALL(a):ALL(b):ALL(c):[(a,b,c) e add1
<=> (a,b,c) e add & ~[a=x & b=0 & c=z]]
Split, 231
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e add1 => e e n & f e n & g e n]
Suppose...
234 (t,u,v) e add1
Premise
235 ALL(b):ALL(c):[(t,b,c) e add1
<=> (t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 233
236 ALL(c):[(t,u,c) e add1
<=> (t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 235
237 (t,u,v) e add1
<=> (t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 236
238 [(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, 237
239 (t,u,v) e add1 => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 238
240 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e add1
Split, 238
241 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 239, 234
242 (t,u,v) e add
Split, 241
243 ~[t=x & u=0 & v=z]
Split, 241
244 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 222
245 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 244
246 (t,u,v) e add => t e n & u e n & v e n
U Spec, 245
247 t e n & u e n & v e n
Detach, 246, 242
As Required:
248 ALL(e):ALL(f):ALL(g):[(e,f,g) e add1 => e e n & f e n & g e n]
4 Conclusion, 234
249 t e n
Premise
250 ALL(b):ALL(c):[(t,b,c) e add1
<=> (t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 233
251 ALL(c):[(t,0,c) e add1
<=> (t,0,c) e add & ~[t=x & 0=0 & c=z]]
U Spec, 250
252 (t,0,t) e add1
<=> (t,0,t) e add & ~[t=x & 0=0 & t=z]
U Spec, 251
253 [(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, 252
254 (t,0,t) e add1 => (t,0,t) e add & ~[t=x & 0=0 & t=z]
Split, 253
255 (t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e add1
Split, 253
256 t e n => (t,0,t) e add
U Spec, 111
257 (t,0,t) e add
Detach, 256, 249
258 t=x & 0=0 & t=z
Premise
259 t=x
Split, 258
260 0=0
Split, 258
261 t=z
Split, 258
262 z=x
Substitute, 261, 259
263 z=x & ~z=x
Join, 262, 226
264 ~[t=x & 0=0 & t=z]
4 Conclusion, 258
265 (t,0,t) e add & ~[t=x & 0=0 & t=z]
Join, 257, 264
266 (t,0,t) e add1
Detach, 255, 265
As Required:
267 ALL(e):[e e n => (e,0,e) e add1]
4 Conclusion, 249
Prove: ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add1 => (e,s(f),s(g)) e add1]]
Suppose...
268 t e n & u e n & v e n & ~u=max & ~v=max
Premise
269 t e n
Split, 268
270 u e n
Split, 268
271 v e n
Split, 268
272 ~u=max
Split, 268
273 ~v=max
Split, 268
Prove: (t,u,v) e add1 => (t,s(u),s(v)) e add1
Suppose...
274 (t,u,v) e add1
Premise
275 ALL(b):ALL(c):[(t,b,c) e add1
<=> (t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 233
276 ALL(c):[(t,u,c) e add1
<=> (t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 275
277 (t,u,v) e add1
<=> (t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 276
278 [(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, 277
279 (t,u,v) e add1 => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 278
280 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e add1
Split, 278
281 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 279, 274
282 (t,u,v) e add
Split, 281
283 ~[t=x & u=0 & v=z]
Split, 281
284 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,b,c) e d]]
U Spec, 199
285 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,c) e d]]
U Spec, 284
286 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,v) e d]
U Spec, 285
287 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,v) e d]
Detach, 286, 282
288 ALL(b):ALL(c):[(t,b,c) e add1
<=> (t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 233
289 ALL(c):[(t,s(u),c) e add1
<=> (t,s(u),c) e add & ~[t=x & s(u)=0 & c=z]]
U Spec, 288
290 (t,s(u),s(v)) e add1
<=> (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
U Spec, 289
291 [(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, 290
292 (t,s(u),s(v)) e add1 => (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
Split, 291
293 (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z] => (t,s(u),s(v)) e add1
Split, 291
294 ALL(b):ALL(c):[t e n & b e n & c e n & ~b=max & ~c=max
=> [(t,b,c) e add => (t,s(b),s(c)) e add]]
U Spec, 165
295 ALL(c):[t e n & u e n & c e n & ~u=max & ~c=max
=> [(t,u,c) e add => (t,s(u),s(c)) e add]]
U Spec, 294
296 t e n & u e n & v e n & ~u=max & ~v=max
=> [(t,u,v) e add => (t,s(u),s(v)) e add]
U Spec, 295
297 (t,u,v) e add => (t,s(u),s(v)) e add
Detach, 296, 268
298 (t,s(u),s(v)) e add
Detach, 297, 282
Prove: ~[t=x & s(u)=0 & s(v)=z]
Suppose to the contrary...
299 t=x & s(u)=0 & s(v)=z
Premise
300 t=x
Split, 299
301 s(u)=0
Split, 299
302 s(v)=z
Split, 299
303 u e n & ~u=max => ~s(u)=0
U Spec, 6
304 u e n & ~u=max
Join, 270, 272
305 ~s(u)=0
Detach, 303, 304
306 s(u)=0 & ~s(u)=0
Join, 301, 305
As Required:
307 ~[t=x & s(u)=0 & s(v)=z]
4 Conclusion, 299
308 (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
Join, 298, 307
309 (t,s(u),s(v)) e add1
Detach, 293, 308
As Required:
310 (t,u,v) e add1 => (t,s(u),s(v)) e add1
4 Conclusion, 274
As Required:
311 ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add1 => (e,s(f),s(g)) e add1]]
4 Conclusion, 268
312 ALL(b):ALL(c):[(x,b,c) e add1
<=> (x,b,c) e add & ~[x=x & b=0 & c=z]]
U Spec, 233
313 ALL(c):[(x,0,c) e add1
<=> (x,0,c) e add & ~[x=x & 0=0 & c=z]]
U Spec, 312
314 (x,0,z) e add1
<=> (x,0,z) e add & ~[x=x & 0=0 & z=z]
U Spec, 313
315 [(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, 314
316 (x,0,z) e add1 => (x,0,z) e add & ~[x=x & 0=0 & z=z]
Split, 315
317 (x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e add1
Split, 315
318 ~[(x,0,z) e add & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e add1
Contra, 316
319 ~~[~(x,0,z) e add | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e add1
DeMorgan, 318
320 ~(x,0,z) e add | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e add1
Rem DNeg, 319
321 ~(x,0,z) e add | x=x & 0=0 & z=z => ~(x,0,z) e add1
Rem DNeg, 320
322 x=x
Reflex
323 0=0
Reflex
324 z=z
Reflex
325 x=x & 0=0
Join, 322, 323
326 x=x & 0=0 & z=z
Join, 325, 324
327 ~(x,0,z) e add | x=x & 0=0 & z=z
Arb Or, 326
As Required:
328 ~(x,0,z) e add1
Detach, 321, 327
329 Set''(add1)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e add1 => e e n & f e n & g e n]
Join, 232, 248
330 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, 329, 267
331 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 & ~f=max & ~g=max
=> [(e,f,g) e add1 => (e,s(f),s(g)) e add1]]
Join, 330, 311
332 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 & ~f=max & ~g=max
=> [(e,f,g) e add1 => (e,s(f),s(g)) e add1]]
& ~(x,0,z) e add1
Join, 331, 328
333 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 & ~f=max & ~g=max
=> [(e,f,g) e d => (e,s(f),s(g)) e d]]
& ~(x,0,z) e d]
E Gen, 332
334 ~(x,0,z) e add
Detach, 229, 333
As Required:
335 ~z=x => ~(x,0,z) e add
4 Conclusion, 226
336 ~~(x,0,z) e add => ~~z=x
Contra, 335
337 (x,0,z) e add => ~~z=x
Rem DNeg, 336
338 (x,0,z) e add => z=x
Rem DNeg, 337
As Required:
339 ALL(a):ALL(c):[a e n & c e n => [(a,0,c) e add => c=a]]
4 Conclusion, 223
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...
340 x e n
Premise
341 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
342 Set(p2) & ALL(b):[b e p2 <=> b e n & EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
E Spec, 341
Define: p2
343 Set(p2)
Split, 342
344 ALL(b):[b e p2 <=> b e n & EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
Split, 342
345 Set(p2) & ALL(b):[b e p2 => b e n]
=> [0 e p2 & ALL(b):[b e p2 & ~b=max => s(b) e p2]
=> ALL(b):[b e n => b e p2]]
U Spec, 8
346 t e p2
Premise
347 t e p2 <=> t e n & EXIST(c):ALL(d):[d e n => [(x,t,d) e add => d=c]]
U Spec, 344
348 [t e p2 => 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 p2]
Iff-And, 347
349 t e p2 => t e n & EXIST(c):ALL(d):[d e n => [(x,t,d) e add => d=c]]
Split, 348
350 t e n & EXIST(c):ALL(d):[d e n => [(x,t,d) e add => d=c]] => t e p2
Split, 348
351 t e n & EXIST(c):ALL(d):[d e n => [(x,t,d) e add => d=c]]
Detach, 349, 346
352 t e n
Split, 351
353 ALL(b):[b e p2 => b e n]
4 Conclusion, 346
354 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 343, 353
Sufficient: ALL(b):[b e n => b e p2]
355 0 e p2 & ALL(b):[b e p2 & ~b=max => s(b) e p2]
=> ALL(b):[b e n => b e p2]
Detach, 345, 354
Base Case
Prove: 0 e p2
356 0 e p2 <=> 0 e n & EXIST(c):ALL(d):[d e n => [(x,0,d) e add => d=c]]
U Spec, 344
357 [0 e p2 => 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 p2]
Iff-And, 356
358 0 e p2 => 0 e n & EXIST(c):ALL(d):[d e n => [(x,0,d) e add => d=c]]
Split, 357
359 0 e n & EXIST(c):ALL(d):[d e n => [(x,0,d) e add => d=c]] => 0 e p2
Split, 357
360 z1 e n
Premise
361 (x,0,z1) e add
Premise
362 ALL(c):[x e n & c e n => [(x,0,c) e add => c=x]]
U Spec, 339
363 x e n & z1 e n => [(x,0,z1) e add => z1=x]
U Spec, 362
364 x e n & z1 e n
Join, 340, 360
365 (x,0,z1) e add => z1=x
Detach, 363, 364
366 z1=x
Detach, 365, 361
367 (x,0,z1) e add => z1=x
4 Conclusion, 361
368 ALL(d):[d e n => [(x,0,d) e add => d=x]]
4 Conclusion, 360
369 EXIST(c):ALL(d):[d e n => [(x,0,d) e add => d=c]]
E Gen, 368
370 0 e n
& EXIST(c):ALL(d):[d e n => [(x,0,d) e add => d=c]]
Join, 2, 369
As Required:
371 0 e p2
Detach, 359, 370
Inductive Step
Prove: ALL(b):[b e p2 & ~b=max => s(b) e p2]
Suppose...
372 y e p2 & ~y=max
Premise
373 y e p2
Split, 372
374 ~y=max
Split, 372
375 y e p2 <=> y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
U Spec, 344
376 [y e p2 => 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 p2]
Iff-And, 375
377 y e p2 => y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Split, 376
378 y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]] => y e p2
Split, 376
379 y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Detach, 377, 373
380 y e n
Split, 379
381 EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Split, 379
382 ALL(d):[d e n => [(x,y,d) e add => d=z]]
E Spec, 381
383 s(y) e p2 <=> s(y) e n & EXIST(c):ALL(d):[d e n => [(x,s(y),d) e add => d=c]]
U Spec, 344
384 [s(y) e p2 => 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 p2]
Iff-And, 383
385 s(y) e p2 => s(y) e n & EXIST(c):ALL(d):[d e n => [(x,s(y),d) e add => d=c]]
Split, 384
Sufficient: s(y) e p2
386 s(y) e n & EXIST(c):ALL(d):[d e n => [(x,s(y),d) e add => d=c]] => s(y) e p2
Split, 384
387 y e n & ~y=max => s(y) e n
U Spec, 5
388 y e n & ~y=max
Join, 380, 374
389 s(y) e n
Detach, 387, 388
Prove: ALL(d):[d e n => [(x,s(y),d) e add => d=s(z)]]
Suppose...
390 z' e n
Premise
Prove: ~z'=s(z) => ~(x,s(y),z') e add
Suppose...
391 ~z'=s(z)
Premise
392 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(x,b,c) e d] => ~(x,b,c) e add]
U Spec, 204
393 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 & ~f=max & ~g=max => [(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, 392
Sufficient: ~(x,s(y),z') e add
394 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 & ~f=max & ~g=max => [(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, 393
395 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, 83
396 Set''(add3) & ALL(a):ALL(b):ALL(c):[(a,b,c) e add3
<=> (a,b,c) e add & ~[a=x & b=s(y) & c=z']]
E Spec, 395
Define: add3 (add without (x,s(y),z'))
************
397 Set''(add3)
Split, 396
398 ALL(a):ALL(b):ALL(c):[(a,b,c) e add3
<=> (a,b,c) e add & ~[a=x & b=s(y) & c=z']]
Split, 396
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
Suppose...
399 (t,u,v) e add3
Premise
400 ALL(b):ALL(c):[(t,b,c) e add3
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 398
401 ALL(c):[(t,u,c) e add3
<=> (t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 400
402 (t,u,v) e add3
<=> (t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 401
403 [(t,u,v) e add3 => (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 add3]
Iff-And, 402
404 (t,u,v) e add3 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 403
405 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e add3
Split, 403
406 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 404, 399
407 (t,u,v) e add
Split, 406
408 ~[t=x & u=s(y) & v=z']
Split, 406
409 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 222
410 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 409
411 (t,u,v) e add => t e n & u e n & v e n
U Spec, 410
412 t e n & u e n & v e n
Detach, 411, 407
As Required:
413 ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
4 Conclusion, 399
Prove: ALL(e):[e e n => (e,0,e) e add3]
Suppose...
414 t e n
Premise
415 ALL(b):ALL(c):[(t,b,c) e add3
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 398
416 ALL(c):[(t,0,c) e add3
<=> (t,0,c) e add & ~[t=x & 0=s(y) & c=z']]
U Spec, 415
417 (t,0,t) e add3
<=> (t,0,t) e add & ~[t=x & 0=s(y) & t=z']
U Spec, 416
418 [(t,0,t) e add3 => (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 add3]
Iff-And, 417
419 (t,0,t) e add3 => (t,0,t) e add & ~[t=x & 0=s(y) & t=z']
Split, 418
420 (t,0,t) e add & ~[t=x & 0=s(y) & t=z'] => (t,0,t) e add3
Split, 418
421 t e n => (t,0,t) e add
U Spec, 111
422 (t,0,t) e add
Detach, 421, 414
423 t=x & 0=s(y) & t=z'
Premise
424 t=x
Split, 423
425 0=s(y)
Split, 423
426 t=z'
Split, 423
427 y e n & ~y=max => ~s(y)=0
U Spec, 6
428 y e n & ~y=max
Join, 380, 374
429 ~s(y)=0
Detach, 427, 428
430 ~0=s(y)
Sym, 429
431 0=s(y) & ~0=s(y)
Join, 425, 430
432 ~[t=x & 0=s(y) & t=z']
4 Conclusion, 423
433 (t,0,t) e add & ~[t=x & 0=s(y) & t=z']
Join, 422, 432
434 (t,0,t) e add3
Detach, 420, 433
As Required:
435 ALL(e):[e e n => (e,0,e) e add3]
4 Conclusion, 414
Prove: ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add3 => (e,s(f),s(g)) e add3]]
Suppose...
436 t e n & u e n & v e n & ~u=max & ~v=max
Premise
437 t e n
Split, 436
438 u e n
Split, 436
439 v e n
Split, 436
440 ~u=max
Split, 436
441 ~v=max
Split, 436
Prove: (t,u,v) e add3 => (t,s(u),s(v)) e add3
Suppose...
442 (t,u,v) e add3
Premise
443 ALL(b):ALL(c):[(t,b,c) e add3
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 398
444 ALL(c):[(t,u,c) e add3
<=> (t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 443
445 (t,u,v) e add3
<=> (t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 444
446 [(t,u,v) e add3 => (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 add3]
Iff-And, 445
447 (t,u,v) e add3 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 446
448 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e add3
Split, 446
449 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 447, 442
450 (t,u,v) e add
Split, 449
451 ~[t=x & u=s(y) & v=z']
Split, 449
452 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,b,c) e d]]
U Spec, 199
453 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,c) e d]]
U Spec, 452
454 (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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,v) e d]
U Spec, 453
455 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 & ~f=max & ~g=max => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (t,u,v) e d]
Detach, 454, 450
456 ALL(b):ALL(c):[(t,b,c) e add3
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 398
457 ALL(c):[(t,s(u),c) e add3
<=> (t,s(u),c) e add & ~[t=x & s(u)=s(y) & c=z']]
U Spec, 456
458 (t,s(u),s(v)) e add3
<=> (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']
U Spec, 457
459 [(t,s(u),s(v)) e add3 => (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 add3]
Iff-And, 458
460 (t,s(u),s(v)) e add3 => (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']
Split, 459
Sufficient:
461 (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z'] => (t,s(u),s(v)) e add3
Split, 459
462 ALL(b):ALL(c):[t e n & b e n & c e n & ~b=max & ~c=max
=> [(t,b,c) e add => (t,s(b),s(c)) e add]]
U Spec, 165
463 ALL(c):[t e n & u e n & c e n & ~u=max & ~c=max
=> [(t,u,c) e add => (t,s(u),s(c)) e add]]
U Spec, 462
464 t e n & u e n & v e n & ~u=max & ~v=max
=> [(t,u,v) e add => (t,s(u),s(v)) e add]
U Spec, 463
465 (t,u,v) e add => (t,s(u),s(v)) e add
Detach, 464, 436
466 (t,s(u),s(v)) e add
Detach, 465, 450
Prove: ~[t=x & s(u)=s(y) & s(v)=z']
Suppose to the contrary...
467 t=x & s(u)=s(y) & s(v)=z'
Premise
468 t=x
Split, 467
469 s(u)=s(y)
Split, 467
470 s(v)=z'
Split, 467
471 ALL(b):[u e n & b e n & ~u=max & ~b=max => [s(u)=s(b) => u=b]]
U Spec, 7
472 u e n & y e n & ~u=max & ~y=max => [s(u)=s(y) => u=y]
U Spec, 471
473 u e n & y e n
Join, 438, 380
474 u e n & y e n & ~u=max
Join, 473, 440
475 u e n & y e n & ~u=max & ~y=max
Join, 474, 374
476 s(u)=s(y) => u=y
Detach, 472, 475
477 u=y
Detach, 476, 469
478 (x,u,v) e add
Substitute, 468, 450
479 (x,y,v) e add
Substitute, 477, 478
480 v e n => [(x,y,v) e add => v=z]
U Spec, 382
481 (x,y,v) e add => v=z
Detach, 480, 439
482 v=z
Detach, 481, 479
483 s(z)=z'
Substitute, 482, 470
484 z'=s(z)
Sym, 483
485 z'=s(z) & ~z'=s(z)
Join, 484, 391
As Required:
486 ~[t=x & s(u)=s(y) & s(v)=z']
4 Conclusion, 467
487 (t,s(u),s(v)) e add
& ~[t=x & s(u)=s(y) & s(v)=z']
Join, 466, 486
488 (t,s(u),s(v)) e add3
Detach, 461, 487
As Required:
489 (t,u,v) e add3 => (t,s(u),s(v)) e add3
4 Conclusion, 442
As Required:
490 ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add3 => (e,s(f),s(g)) e add3]]
4 Conclusion, 436
491 ALL(b):ALL(c):[(x,b,c) e add3
<=> (x,b,c) e add & ~[x=x & b=s(y) & c=z']]
U Spec, 398
492 ALL(c):[(x,s(y),c) e add3
<=> (x,s(y),c) e add & ~[x=x & s(y)=s(y) & c=z']]
U Spec, 491
493 (x,s(y),z') e add3
<=> (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
U Spec, 492
494 [(x,s(y),z') e add3 => (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 add3]
Iff-And, 493
495 (x,s(y),z') e add3 => (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
Split, 494
496 (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e add3
Split, 494
497 ~[(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e add3
Contra, 495
498 ~~[~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e add3
DeMorgan, 497
499 ~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z'] => ~(x,s(y),z') e add3
Rem DNeg, 498
500 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z' => ~(x,s(y),z') e add3
Rem DNeg, 499
501 x=x
Reflex
502 s(y)=s(y)
Reflex
503 z'=z'
Reflex
504 x=x & s(y)=s(y)
Join, 501, 502
505 x=x & s(y)=s(y) & z'=z'
Join, 504, 503
506 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z'
Arb Or, 505
As Required:
507 ~(x,s(y),z') e add3
Detach, 500, 506
508 Set''(add3)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
Join, 397, 413
509 Set''(add3)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
& ALL(e):[e e n => (e,0,e) e add3]
Join, 508, 435
510 Set''(add3)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
& ALL(e):[e e n => (e,0,e) e add3]
& ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add3 => (e,s(f),s(g)) e add3]]
Join, 509, 490
511 Set''(add3)
& ALL(e):ALL(f):ALL(g):[(e,f,g) e add3 => e e n & f e n & g e n]
& ALL(e):[e e n => (e,0,e) e add3]
& ALL(e):ALL(f):ALL(g):[e e n & f e n & g e n & ~f=max & ~g=max
=> [(e,f,g) e add3 => (e,s(f),s(g)) e add3]]
& ~(x,s(y),z') e add3
Join, 510, 507
512 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 & ~f=max & ~g=max
=> [(e,f,g) e d => (e,s(f),s(g)) e d]]
& ~(x,s(y),z') e d]
E Gen, 511
513 ~(x,s(y),z') e add
Detach, 394, 512
As Required:
514 ~z'=s(z) => ~(x,s(y),z') e add
4 Conclusion, 391
515 ~~(x,s(y),z') e add => ~~z'=s(z)
Contra, 514
516 (x,s(y),z') e add => ~~z'=s(z)
Rem DNeg, 515
517 (x,s(y),z') e add => z'=s(z)
Rem DNeg, 516
As Required:
518 ALL(d):[d e n => [(x,s(y),d) e add => d=s(z)]]
4 Conclusion, 390
519 EXIST(c):ALL(d):[d e n => [(x,s(y),d) e add => d=c]]
E Gen, 518
520 s(y) e n
& EXIST(c):ALL(d):[d e n => [(x,s(y),d) e add => d=c]]
Join, 389, 519
521 s(y) e p2
Detach, 386, 520
As Required:
522 ALL(b):[b e p2 & ~b=max => s(b) e p2]
4 Conclusion, 372
523 0 e p2 & ALL(b):[b e p2 & ~b=max => s(b) e p2]
Join, 371, 522
As Required:
524 ALL(b):[b e n => b e p2]
Detach, 355, 523
Prove: ALL(b):[b e n
=> EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
Suppose...
525 y e n
Premise
526 y e n => y e p2
U Spec, 524
527 y e p2
Detach, 526, 525
528 y e p2 <=> y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
U Spec, 344
529 [y e p2 => 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 p2]
Iff-And, 528
530 y e p2 => y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Split, 529
531 y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]] => y e p2
Split, 529
532 y e n & EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Detach, 530, 527
533 y e n
Split, 532
534 EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Split, 532
As Required:
535 ALL(b):[b e n
=> EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
4 Conclusion, 525
As Required:
536 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, 340
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]]
Suppose...
537 x e n & y e n & z1 e n & z2 e n
Premise
538 x e n
Split, 537
539 y e n
Split, 537
540 z1 e n
Split, 537
541 z2 e n
Split, 537
Prove: (x,y,z1) e add & (x,y,z2) e add => z1=z2
Suppose...
542 (x,y,z1) e add & (x,y,z2) e add
Premise
543 (x,y,z1) e add
Split, 542
544 (x,y,z2) e add
Split, 542
545 x e n
=> ALL(b):[b e n
=> EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
U Spec, 536
546 ALL(b):[b e n
=> EXIST(c):ALL(d):[d e n => [(x,b,d) e add => d=c]]]
Detach, 545, 538
547 y e n
=> EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
U Spec, 546
548 EXIST(c):ALL(d):[d e n => [(x,y,d) e add => d=c]]
Detach, 547, 539
549 ALL(d):[d e n => [(x,y,d) e add => d=z]]
E Spec, 548
550 z1 e n => [(x,y,z1) e add => z1=z]
U Spec, 549
551 (x,y,z1) e add => z1=z
Detach, 550, 540
552 z1=z
Detach, 551, 543
553 z2 e n => [(x,y,z2) e add => z2=z]
U Spec, 549
554 (x,y,z2) e add => z2=z
Detach, 553, 541
555 z2=z
Detach, 554, 544
556 z1=z2
Substitute, 555, 552
As Required:
557 (x,y,z1) e add & (x,y,z2) e add => z1=z2
4 Conclusion, 542
As Required:
558 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, 537