Constructing the ADD Function
Construct the add function for the natural numbers given Peano's Axioms.
(F5 to view highlights only)
Peano's axioms for the natural numbers
1 Set(n)
& 1
n
& ALL(a):[an => next(a)n]
& ALL(a):[an => ~next(a)=1]
& ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
& ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
=> ALL(b):[bn => ba]]
Premise
Splitting...
2 Set(n)
Split, 1
3 1n
Split, 1
4 ALL(a):[an => next(a)n]
Split, 1
5 ALL(a):[an => ~next(a)=1]
Split, 1
6 ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
Split, 1
7 ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
=> ALL(b):[bn => ba]]
Split, 1
Construct the set of ordered triples of natural numbers, n3
Applying the Cartesian Product rule...
8 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)b <=> c1a1 & c2a2 & c3a3]]]
Cart Prod
9 ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2a2 & c3a3]]]
U Spec, 8
10 ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3a3]]]
U Spec, 9
11 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3n]]
U Spec, 10
12 Set(n) & Set(n)
Join, 2, 2
13 Set(n) & Set(n) & Set(n)
Join, 12, 2
14 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3n]]
Detach, 11, 13
Define: n3, the set of ordered triples of natural numbers
15 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
E Spec, 14
16 Set''(n3)
Split, 15
17 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
Split, 15
Construct the add function, a subset of n3
Applying the Subset rule...
18 EXIST(s):[Set''(s) & ALL(a):ALL(b):ALL(c):[(a,b,c)s
<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')s & next(b')=b & next(c')=c]]]]
Subset, 16
Define: add, a subset of n3
19 Set''(add) & ALL(a):ALL(b):ALL(c):[(a,b,c)add
<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')add & next(b')=b & next(c')=c]]]
E Spec, 18
20 Set''(add)
Split, 19
21 ALL(a):ALL(b):ALL(c):[(a,b,c)add
<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')add & next(b')=b & next(c')=c]]]
Split, 19
Prove: Add is a function
Applying the definiton of functionality...
22 ALL(f):ALL(a1):ALL(a2):ALL(b):[Set''(f)
& Set(a1) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1a1 & c2a2 => EXIST(d):[db & (c1,c2,d)f]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1a1 & c2a2 & d1b & d2b & (c1,c2,d1)f & (c1,c2,d2)f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1a1 & c2a2 & db => [d=f(c1,c2) <=> (c1,c2,d)f]]]
Function
23 ALL(a1):ALL(a2):ALL(b):[Set''(add)
& Set(a1) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1a1 & c2a2 => EXIST(d):[db & (c1,c2,d)add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1a1 & c2a2 & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1a1 & c2a2 & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
U Spec, 22
24 ALL(a2):ALL(b):[Set''(add)
& Set(n) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1n & c2a2 => EXIST(d):[db & (c1,c2,d)add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2a2 & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2a2 & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
U Spec, 23
25 ALL(b):[Set''(add)
& Set(n) & Set(n) & Set(b)
& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[db & (c1,c2,d)add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
U Spec, 24
Sufficient: For functionality of add
26 Set''(add)
& Set(n) & Set(n) & Set(n)
& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[dn & (c1,c2,d)add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & dn => [d=add(c1,c2) <=> (c1,c2,d)add]]
U Spec, 25
Prove: xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
Suppose...
27 xn
Premise
Sufficient: For ALL(y):[yn => EXIST(z):[dn & (x,y,z)add]]
Apply the Induction shortcut (on Numbers menu).
28 EXIST(z):[zn & (x,1,z)add] & ALL(y):[yn & EXIST(z):[zn & (x,y,z)add]
=> EXIST(z):[zn & (x,next(y),z)add]]
=> ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
Induction
Prove: (x,1,next(x))add (the case for y=1)
Applying the definition add...
29 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
30 ALL(c):[(x,1,c)add
<=> (x,1,c)n3 & [1=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=c]]]
U Spec, 29
31 (x,1,next(x))add
<=> (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
U Spec, 30
32 [(x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]]
& [(x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add]
Iff-And, 31
33 (x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
Split, 32
Sufficient: For (x,1,next(x))add
34 (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add
Split, 32
Prove: (x,1,next(x))n3
Applying the definition of n3...
35 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 17
36 ALL(c3):[(x,1,c3)n3 <=> xn & 1n & c3n]
U Spec, 35
37 (x,1,next(x))n3 <=> xn & 1n & next(x)n
U Spec, 36
38 [(x,1,next(x))n3 => xn & 1n & next(x)n]
& [xn & 1n & next(x)n => (x,1,next(x))n3]
Iff-And, 37
39 (x,1,next(x))n3 => xn & 1n & next(x)n
Split, 38
Sufficient: For (x,1,next(x))n3
40 xn & 1n & next(x)n => (x,1,next(x))n3
Split, 38
41 xn => next(x)n
U Spec, 4
42 next(x)n
Detach, 41, 27
43 xn & 1n
Join, 27, 3
44 xn & 1n & next(x)n
Join, 43, 42
As Required:
45 (x,1,next(x))n3
Detach, 40, 44
Prove: 1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]
46 1=1
Reflex
47 next(x)=next(x)
Reflex
48 1=1 & next(x)=next(x)
Join, 46, 47
As Required:
49 1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]
Arb Or, 48
50 (x,1,next(x))n3
& [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
Join, 45, 49
51 (x,1,next(x))add
Detach, 34, 50
52 next(x)n & (x,1,next(x))add
Join, 42, 51
As Required: The case for y=1
53 EXIST(z):[zn & (x,1,z)add]
E Gen, 52
Prove: yn & EXIST(z):[zn & (x,y,z)add]
=> EXIST(z):[zn & (x,next(y),z)add]
The case for if true for y, then true for next(y) (y+1)
Suppose...
54 yn & EXIST(z):[zn & (x,y,z)add]
Premise
55 yn
Split, 54
56 EXIST(z):[zn & (x,y,z)add]
Split, 54
Define: z
57 zn & (x,y,z)add
E Spec, 56
58 zn
Split, 57
59 (x,y,z)add
Split, 57
Prove: (x,next(y),next(z))add
Applying the definition of add...
60 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
61 ALL(c):[(x,next(y),c)add
<=> (x,next(y),c)n3 & [next(y)=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=c]]]
U Spec, 60
62 (x,next(y),next(z))add
<=> (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]
U Spec, 61
63 [(x,next(y),next(z))add => (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]]
& [(x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]] => (x,next(y),next(z))add]
Iff-And, 62
64 (x,next(y),next(z))add => (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]
Split, 63
Sufficient: For (x,next(y),next(z))add
65 (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]] => (x,next(y),next(z))add
Split, 63
Prove: (x,next(y),next(z))n3
Applying the definition of n3...
66 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 17
67 ALL(c3):[(x,next(y),c3)n3 <=> xn & next(y)n & c3n]
U Spec, 66
68 (x,next(y),next(z))n3 <=> xn & next(y)n & next(z)n
U Spec, 67
69 [(x,next(y),next(z))n3 => xn & next(y)n & next(z)n]
& [xn & next(y)n & next(z)n => (x,next(y),next(z))n3]
Iff-And, 68
70 (x,next(y),next(z))n3 => xn & next(y)n & next(z)n
Split, 69
Sufficient: For (x,next(y),next(z))n3
71 xn & next(y)n & next(z)n => (x,next(y),next(z))n3
Split, 69
72 yn => next(y)n
U Spec, 4
73 next(y)n
Detach, 72, 55
74 zn => next(z)n
U Spec, 4
75 next(z)n
Detach, 74, 58
76 xn & next(y)n
Join, 27, 73
77 xn & next(y)n & next(z)n
Join, 76, 75
As Required:
78 (x,next(y),next(z))n3
Detach, 71, 77
Prove: EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y) & next(c)=next(z)]
79 next(y)=next(y)
Reflex
80 next(z)=next(z)
Reflex
81 yn & zn
Join, 55, 58
82 yn & zn & (x,y,z)add
Join, 81, 59
83 yn & zn & (x,y,z)add & next(y)=next(y)
Join, 82, 79
84 yn & zn & (x,y,z)add & next(y)=next(y)
& next(z)=next(z)
Join, 83, 80
85 EXIST(c):[yn & cn & (x,y,c)add & next(y)=next(y)
& next(c)=next(z)]
E Gen, 84
As Required:
86 EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y)
& next(c)=next(z)]
E Gen, 85
87 next(y)=1 & next(x)=next(z) | EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y)
& next(c)=next(z)]
Arb Or, 86
88 (x,next(y),next(z))n3
& [next(y)=1 & next(x)=next(z) | EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y)
& next(c)=next(z)]]
Join, 78, 87
As Required:
89 (x,next(y),next(z))add
Detach, 65, 88
90 next(z)n & (x,next(y),next(z))add
Join, 75, 89
91 EXIST(c):[cn & (x,next(y),c)add]
E Gen, 90
As Required:
The case for if true for y, then true for next(y) (y+1)
92 yn & EXIST(z):[zn & (x,y,z)add]
=> EXIST(c):[cn & (x,next(y),c)add]
Conclusion, 54
Generalizing...
93 ALL(y):[yn & EXIST(z):[zn & (x,y,z)add]
=> EXIST(c):[cn & (x,next(y),c)add]]
U Gen, 92
94 EXIST(z):[zn & (x,1,z)add]
& ALL(y):[yn & EXIST(z):[zn & (x,y,z)add]
=> EXIST(c):[cn & (x,next(y),c)add]]
Join, 53, 93
By induction...
95 ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
Detach, 28, 94
As Required:
96 xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
Conclusion, 27
Generalizing...
97 ALL(x):[xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]]
U Gen, 96
Prove: xn & yn => EXIST(z):[zn & (x,y,z)add]
Suppose...
98 xn & yn
Premise
99 xn
Split, 98
100 yn
Split, 98
101 xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
U Spec, 97
102 ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
Detach, 101, 99
103 yn => EXIST(z):[zn & (x,y,z)add]
U Spec, 102
104 EXIST(z):[zn & (x,y,z)add]
Detach, 103, 100
As Required:
105 xn & yn => EXIST(z):[zn & (x,y,z)add]
Conclusion, 98
Generalizing...
106 ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
U Gen, 105
As Required:
Every order pair of natural numbers has an image under add.
107 ALL(x):ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
U Gen, 106
Prove: xn => ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]]
Suppose...
108 xn
Premise
Sufficient: ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
Applying the Induction shortcut...
109 ALL(z1):ALL(z2):[z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2]
& ALL(y):[yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
=> ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add => z1=z2]]
=> ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]]
Induction
Prove: z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2 (Case for y=1)
Suppose...
110 z1n & z2n & (x,1,z1)add & (x,1,z2)add
Premise
111 z1n
Split, 110
112 z2n
Split, 110
113 (x,1,z1)add
Split, 110
114 (x,1,z2)add
Split, 110
Applying the definition of add...
115 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
116 ALL(c):[(x,1,c)add
<=> (x,1,c)n3 & [1=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=c]]]
U Spec, 115
117 (x,1,z1)add
<=> (x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]]
U Spec, 116
118 [(x,1,z1)add => (x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]]]
& [(x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]] => (x,1,z1)add]
Iff-And, 117
119 (x,1,z1)add => (x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]]
Split, 118
120 (x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]] => (x,1,z1)add
Split, 118
121 (x,1,z1)n3 & [1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]]
Detach, 119, 113
122 (x,1,z1)n3
Split, 121
123 1=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Split, 121
124 ~[1=1 & next(x)=z1] => EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Imply-Or, 123
125 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1] => ~~[1=1 & next(x)=z1]
Contra, 124
Sufficient: For next(x)=z1
126 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1] => 1=1 & next(x)=z1
Rem DNeg, 125
Applying the definition of add...
127 (x,1,z2)add
<=> (x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]]
U Spec, 116
128 [(x,1,z2)add => (x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]]]
& [(x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]] => (x,1,z2)add]
Iff-And, 127
129 (x,1,z2)add => (x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]]
Split, 128
130 (x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]] => (x,1,z2)add
Split, 128
From the definition of add...
131 (x,1,z2)n3 & [1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]]
Detach, 129, 114
132 (x,1,z2)n3
Split, 131
133 1=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Split, 131
134 ~[1=1 & next(x)=z2] => EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Imply-Or, 133
135 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2] => ~~[1=1 & next(x)=z2]
Contra, 134
Sufficient: For next(x)=z2
136 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2] => 1=1 & next(x)=z2
Rem DNeg, 135
137 b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1
Premise
138 b'n
Split, 137
139 c'n
Split, 137
140 (x,b',c')add
Split, 137
141 next(b')=1
Split, 137
142 next(c')=z1
Split, 137
143 b'n => ~next(b')=1
U Spec, 5
144 ~next(b')=1
Detach, 143, 138
145 next(b')=1 & ~next(b')=1
Join, 141, 144
146 ~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Conclusion, 137
147 ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
U Gen, 146
148 ALL(b'):ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
U Gen, 147
149 ~EXIST(b'):~ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Quant, 148
150 ~EXIST(b'):~~EXIST(c'):~~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Quant, 149
151 ~EXIST(b'):EXIST(c'):~~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Rem DNeg, 150
152 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z1]
Rem DNeg, 151
153 1=1 & next(x)=z1
Detach, 126, 152
154 1=1
Split, 153
As Required:
155 next(x)=z1
Split, 153
156 b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2
Premise
157 b'n
Split, 156
158 c'n
Split, 156
159 (x,b',c')add
Split, 156
160 next(b')=1
Split, 156
161 next(c')=z2
Split, 156
162 b'n => ~next(b')=1
U Spec, 5
163 ~next(b')=1
Detach, 162, 157
164 next(b')=1 & ~next(b')=1
Join, 160, 163
165 ~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Conclusion, 156
166 ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
U Gen, 165
167 ALL(b'):ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
U Gen, 166
168 ~EXIST(b'):~ALL(c'):~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Quant, 167
169 ~EXIST(b'):~~EXIST(c'):~~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Quant, 168
170 ~EXIST(b'):EXIST(c'):~~[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Rem DNeg, 169
171 ~EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=z2]
Rem DNeg, 170
172 1=1 & next(x)=z2
Detach, 136, 171
173 1=1
Split, 172
174 next(x)=z2
Split, 172
175 z1=z2
Substitute, 155, 174
As Required:
176 z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2
Conclusion, 110
Generalizing...
177 ALL(z2):[z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2]
U Gen, 176
Case for y=1:
178 ALL(z1):ALL(z2):[z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2]
U Gen, 177
Prove: yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
=> ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add => z1=z2]
Suppose...
179 yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
Premise
180 yn
Split, 179
181 ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
Split, 179
Prove: z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add => z1=z2
Suppose...
182 z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
Premise
183 z1n
Split, 182
184 z2n
Split, 182
185 (x,next(y),z1)add
Split, 182
186 (x,next(y),z2)add
Split, 182
187 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
188 ALL(c):[(x,next(y),c)add
<=> (x,next(y),c)n3 & [next(y)=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=c]]]
U Spec, 187
189 (x,next(y),z1)add
<=> (x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]]
U Spec, 188
190 [(x,next(y),z1)add => (x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]]]
& [(x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]] => (x,next(y),z1)add]
Iff-And, 189
191 (x,next(y),z1)add => (x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]]
Split, 190
192 (x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]] => (x,next(y),z1)add
Split, 190
193 (x,next(y),z1)n3 & [next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]]
Detach, 191, 185
From the definition of add...
194 (x,next(y),z1)n3
Split, 193
195 next(y)=1 & next(x)=z1 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]
Split, 193
196 (x,next(y),z2)add
<=> (x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]]
U Spec, 188
197 [(x,next(y),z2)add => (x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]]]
& [(x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]] => (x,next(y),z2)add]
Iff-And, 196
198 (x,next(y),z2)add => (x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]]
Split, 197
199 (x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]] => (x,next(y),z2)add
Split, 197
200 (x,next(y),z2)n3 & [next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]]
Detach, 198, 186
201 (x,next(y),z2)n3
Split, 200
202 next(y)=1 & next(x)=z2 | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]
Split, 200
203 ~[next(y)=1 & next(x)=z1] => EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]
Imply-Or, 195
204 next(y)=1 & next(x)=z1
Premise
205 next(y)=1
Split, 204
206 next(x)=z1
Split, 204
207 yn => ~next(y)=1
U Spec, 5
208 ~next(y)=1
Detach, 207, 180
209 next(y)=1 & ~next(y)=1
Join, 205, 208
210 ~[next(y)=1 & next(x)=z1]
Conclusion, 204
211 EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z1]
Detach, 203, 210
212 ~[next(y)=1 & next(x)=z2] => EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]
Imply-Or, 202
213 next(y)=1 & next(x)=z2
Premise
214 next(y)=1
Split, 213
215 next(x)=z2
Split, 213
216 yn => ~next(y)=1
U Spec, 5
217 ~next(y)=1
Detach, 216, 180
218 next(y)=1 & ~next(y)=1
Join, 214, 217
219 ~[next(y)=1 & next(x)=z2]
Conclusion, 213
220 EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=z2]
Detach, 212, 219
221 EXIST(c'):[y1'n & c'n & (x,y1',c')add & next(y1')=next(y) & next(c')=z1]
E Spec, 211
Define: y1' and z1'
222 y1'n & z1'n & (x,y1',z1')add & next(y1')=next(y) & next(z1')=z1
E Spec, 221
223 y1'n
Split, 222
224 z1'n
Split, 222
225 (x,y1',z1')add
Split, 222
226 next(y1')=next(y)
Split, 222
227 next(z1')=z1
Split, 222
228 EXIST(c'):[y2'n & c'n & (x,y2',c')add & next(y2')=next(y) & next(c')=z2]
E Spec, 220
Define: y2' and z2'
229 y2'n & z2'n & (x,y2',z2')add & next(y2')=next(y) & next(z2')=z2
E Spec, 228
230 y2'n
Split, 229
231 z2'n
Split, 229
232 (x,y2',z2')add
Split, 229
233 next(y2')=next(y)
Split, 229
234 next(z2')=z2
Split, 229
235 ALL(b):[y1'n & bn & next(y1')=next(b) => y1'=b]
U Spec, 6
236 y1'n & yn & next(y1')=next(y) => y1'=y
U Spec, 235
237 y1'n & yn
Join, 223, 180
238 y1'n & yn & next(y1')=next(y)
Join, 237, 226
239 y1'=y
Detach, 236, 238
240 (x,y,z1')add
Substitute, 239, 225
241 ALL(b):[y2'n & bn & next(y2')=next(b) => y2'=b]
U Spec, 6
242 y2'n & yn & next(y2')=next(y) => y2'=y
U Spec, 241
243 y2'n & yn
Join, 230, 180
244 y2'n & yn & next(y2')=next(y)
Join, 243, 233
245 y2'=y
Detach, 242, 244
246 (x,y,z2')add
Substitute, 245, 232
247 ALL(z2):[z1'n & z2n & (x,y,z1')add & (x,y,z2)add => z1'=z2]
U Spec, 181
248 z1'n & z2'n & (x,y,z1')add & (x,y,z2')add => z1'=z2'
U Spec, 247
249 z1'n & z2'n
Join, 224, 231
250 z1'n & z2'n & (x,y,z1')add
Join, 249, 240
251 z1'n & z2'n & (x,y,z1')add & (x,y,z2')add
Join, 250, 246
252 z1'=z2'
Detach, 248, 251
253 next(z1')=z2
Substitute, 252, 234
254 z1=z2
Substitute, 227, 253
255 z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2
Conclusion, 182
256 ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2]
U Gen, 255
257 ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2]
U Gen, 256
As Required:
258 yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
=> ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2]
Conclusion, 179
Generalizing...
259 ALL(y):[yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
=> ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2]]
U Gen, 258
260 ALL(z1):ALL(z2):[z1n & z2n & (x,1,z1)add & (x,1,z2)add => z1=z2]
& ALL(y):[yn & ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]
=> ALL(z1):ALL(z2):[z1n & z2n & (x,next(y),z1)add & (x,next(y),z2)add
=> z1=z2]]
Join, 178, 259
261 ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]]
Detach, 109, 260
As Required:
262 xn
=> ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]]
Conclusion, 108
Generalizing...
263 ALL(x):[xn
=> ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (x,y,z1)add & (x,y,z2)add => z1=z2]]]
U Gen, 262
264 c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
Premise
265 c1n
Split, 264
266 c2n
Split, 264
267 d1n
Split, 264
268 d2n
Split, 264
269 (c1,c2,d1)add
Split, 264
270 (c1,c2,d2)add
Split, 264
271 c1n
=> ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (c1,y,z1)add & (c1,y,z2)add => z1=z2]]
U Spec, 263
272 ALL(y):[yn => ALL(z1):ALL(z2):[z1n & z2n & (c1,y,z1)add & (c1,y,z2)add => z1=z2]]
Detach, 271, 265
273 c2n => ALL(z1):ALL(z2):[z1n & z2n & (c1,c2,z1)add & (c1,c2,z2)add => z1=z2]
U Spec, 272
274 ALL(z1):ALL(z2):[z1n & z2n & (c1,c2,z1)add & (c1,c2,z2)add => z1=z2]
Detach, 273, 266
275 ALL(z2):[d1n & z2n & (c1,c2,d1)add & (c1,c2,z2)add => d1=z2]
U Spec, 274
276 d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2
U Spec, 275
277 d1n & d2n
Join, 267, 268
278 d1n & d2n & (c1,c2,d1)add
Join, 277, 269
279 d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
Join, 278, 270
280 d1=d2
Detach, 276, 279
As Required:
281 c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2
Conclusion, 264
Generalizing...
282 ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2]
U Gen, 281
283 ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2]
U Gen, 282
284 ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2]
U Gen, 283
285 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2]
U Gen, 284
Joining results...
286 Set''(add) & Set(n)
Join, 20, 2
287 Set''(add) & Set(n) & Set(n)
Join, 286, 2
288 Set''(add) & Set(n) & Set(n) & Set(n)
Join, 287, 2
289 Set''(add) & Set(n) & Set(n) & Set(n)
& ALL(x):ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
Join, 288, 107
290 Set''(add) & Set(n) & Set(n) & Set(n)
& ALL(x):ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add
=> d1=d2]
Join, 289, 285
As Required: add is a function
291 ALL(c1):ALL(c2):ALL(d):[c1n & c2n & dn => [d=add(c1,c2) <=> (c1,c2,d)add]]
Detach, 26, 290
Prove: xn & yn => add(x,y)n
Suppose...
292 xn & yn
Premise
293 xn
Split, 292
294 yn
Split, 292
295 ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
U Spec, 107
296 xn & yn => EXIST(z):[zn & (x,y,z)add]
U Spec, 295
297 EXIST(z):[zn & (x,y,z)add]
Detach, 296, 292
298 zn & (x,y,z)add
E Spec, 297
299 zn
Split, 298
300 (x,y,z)add
Split, 298
301 ALL(c2):ALL(d):[xn & c2n & dn => [d=add(x,c2) <=> (x,c2,d)add]]
U Spec, 291
302 ALL(d):[xn & yn & dn => [d=add(x,y) <=> (x,y,d)add]]
U Spec, 301
303 xn & yn & zn => [z=add(x,y) <=> (x,y,z)add]
U Spec, 302
304 xn & yn & zn
Join, 292, 299
305 z=add(x,y) <=> (x,y,z)add
Detach, 303, 304
306 [z=add(x,y) => (x,y,z)add]
& [(x,y,z)add => z=add(x,y)]
Iff-And, 305
307 z=add(x,y) => (x,y,z)add
Split, 306
308 (x,y,z)add => z=add(x,y)
Split, 306
309 z=add(x,y)
Detach, 308, 300
310 add(x,y)n
Substitute, 309, 299
As Required:
311 xn & yn => add(x,y)n
Conclusion, 292
Generalizing...
312 ALL(b):[xn & bn => add(x,b)n]
U Gen, 311
313 ALL(a):ALL(b):[an & bn => add(a,b)n]
U Gen, 312
Prove: xn => add(x,1)=next(x)
Suppose...
314 xn
Premise
Prove: (x,1,next(x))add
Applying the definitin of add...
315 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
316 ALL(c):[(x,1,c)add
<=> (x,1,c)n3 & [1=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=c]]]
U Spec, 315
317 (x,1,next(x))add
<=> (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
U Spec, 316
318 [(x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]]
& [(x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add]
Iff-And, 317
319 (x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
Split, 318
Sufficient: For (x,1,next(x))add
320 (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add
Split, 318
321 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 17
322 ALL(c3):[(x,1,c3)n3 <=> xn & 1n & c3n]
U Spec, 321
323 (x,1,next(x))n3 <=> xn & 1n & next(x)n
U Spec, 322
324 [(x,1,next(x))n3 => xn & 1n & next(x)n]
& [xn & 1n & next(x)n => (x,1,next(x))n3]
Iff-And, 323
325 (x,1,next(x))n3 => xn & 1n & next(x)n
Split, 324
Sufficient: For (x,1,next(x))n3
326 xn & 1n & next(x)n => (x,1,next(x))n3
Split, 324
327 xn => next(x)n
U Spec, 4
328 next(x)n
Detach, 327, 314
329 xn & 1n
Join, 314, 3
330 xn & 1n & next(x)n
Join, 329, 328
As Required:
331 (x,1,next(x))n3
Detach, 326, 330
332 1=1
Reflex
333 next(x)=next(x)
Reflex
334 1=1 & next(x)=next(x)
Join, 332, 333
335 1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]
Arb Or, 334
336 (x,1,next(x))n3
& [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
Join, 331, 335
337 (x,1,next(x))add
Detach, 320, 336
338 ALL(c2):ALL(d):[xn & c2n & dn => [d=add(x,c2) <=> (x,c2,d)add]]
U Spec, 291
339 ALL(d):[xn & 1n & dn => [d=add(x,1) <=> (x,1,d)add]]
U Spec, 338
340 xn & 1n & next(x)n => [next(x)=add(x,1) <=> (x,1,next(x))add]
U Spec, 339
341 next(x)=add(x,1) <=> (x,1,next(x))add
Detach, 340, 330
342 [next(x)=add(x,1) => (x,1,next(x))add]
& [(x,1,next(x))add => next(x)=add(x,1)]
Iff-And, 341
343 next(x)=add(x,1) => (x,1,next(x))add
Split, 342
344 (x,1,next(x))add => next(x)=add(x,1)
Split, 342
345 next(x)=add(x,1)
Detach, 344, 337
346 add(x,1)=next(x)
Sym, 345
As Required:
347 xn => add(x,1)=next(x)
Conclusion, 314
Generalizing...
348 ALL(a):[an => add(a,1)=next(a)]
U Gen, 347
Prove: xn & yn => add(x,next(y))=next(add(x,y))
Suppose...
349 xn & yn
Premise
350 xn
Split, 349
351 yn
Split, 349
Applying the definition of add...
352 ALL(b):ALL(c):[(x,b,c)add
<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
U Spec, 21
353 ALL(c):[(x,next(y),c)add
<=> (x,next(y),c)n3 & [next(y)=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=c]]]
U Spec, 352
354 (x,next(y),next(add(x,y)))add
<=> (x,next(y),next(add(x,y)))n3 & [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(add(x,y))]]
U Spec, 353
355 [(x,next(y),next(add(x,y)))add => (x,next(y),next(add(x,y)))n3 & [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(add(x,y))]]]
& [(x,next(y),next(add(x,y)))n3 & [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(add(x,y))]] => (x,next(y),next(add(x,y)))add]
Iff-And, 354
356 (x,next(y),next(add(x,y)))add => (x,next(y),next(add(x,y)))n3 & [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(add(x,y))]]
Split, 355
Sufficient: For (x,next(y),next(add(x,y)))add
357 (x,next(y),next(add(x,y)))n3 & [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(add(x,y))]] => (x,next(y),next(add(x,y)))add
Split, 355
358 ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
U Spec, 107
359 xn & yn => EXIST(z):[zn & (x,y,z)add]
U Spec, 358
360 EXIST(z):[zn & (x,y,z)add]
Detach, 359, 349
361 zn & (x,y,z)add
E Spec, 360
362 zn
Split, 361
363 (x,y,z)add
Split, 361
364 ALL(b):[xn & bn => add(x,b)n]
U Spec, 313
365 xn & yn => add(x,y)n
U Spec, 364
366 add(x,y)n
Detach, 365, 349
367 ALL(c2):ALL(d):[xn & c2n & dn => [d=add(x,c2) <=> (x,c2,d)add]]
U Spec, 291
368 ALL(d):[xn & yn & dn => [d=add(x,y) <=> (x,y,d)add]]
U Spec, 367
369 xn & yn & zn => [z=add(x,y) <=> (x,y,z)add]
U Spec, 368
370 xn & yn & zn
Join, 349, 362
371 z=add(x,y) <=> (x,y,z)add
Detach, 369, 370
372 [z=add(x,y) => (x,y,z)add]
& [(x,y,z)add => z=add(x,y)]
Iff-And, 371
373 z=add(x,y) => (x,y,z)add
Split, 372
374 (x,y,z)add => z=add(x,y)
Split, 372
375 z=add(x,y)
Detach, 374, 363
376 (x,y,add(x,y))add
Substitute, 375, 363
377 next(y)=next(y)
Reflex
378 next(add(x,y))=next(add(x,y))
Reflex
379 yn & add(x,y)n
Join, 351, 366
380 yn & add(x,y)n & (x,y,add(x,y))add
Join, 379, 376
381 yn & add(x,y)n & (x,y,add(x,y))add
& next(y)=next(y)
Join, 380, 377
382 yn & add(x,y)n & (x,y,add(x,y))add
& next(y)=next(y)
& next(add(x,y))=next(add(x,y))
Join, 381, 378
383 EXIST(c'):[yn & c'n & (x,y,c')add
& next(y)=next(y)
& next(c')=next(add(x,y))]
E Gen, 382
384 EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add
& next(b')=next(y)
& next(c')=next(add(x,y))]
E Gen, 383
385 next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add
& next(b')=next(y)
& next(c')=next(add(x,y))]
Arb Or, 384
386 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 17
387 ALL(c3):[(x,next(y),c3)n3 <=> xn & next(y)n & c3n]
U Spec, 386
388 (x,next(y),next(add(x,y)))n3 <=> xn & next(y)n & next(add(x,y))n
U Spec, 387
389 [(x,next(y),next(add(x,y)))n3 => xn & next(y)n & next(add(x,y))n]
& [xn & next(y)n & next(add(x,y))n => (x,next(y),next(add(x,y)))n3]
Iff-And, 388
390 (x,next(y),next(add(x,y)))n3 => xn & next(y)n & next(add(x,y))n
Split, 389
Sufficient:
391 xn & next(y)n & next(add(x,y))n => (x,next(y),next(add(x,y)))n3
Split, 389
392 yn => next(y)n
U Spec, 4
393 next(y)n
Detach, 392, 351
394 add(x,y)n => next(add(x,y))n
U Spec, 4
395 next(add(x,y))n
Detach, 394, 366
396 xn & next(y)n
Join, 350, 393
397 xn & next(y)n & next(add(x,y))n
Join, 396, 395
As Required:
398 (x,next(y),next(add(x,y)))n3
Detach, 391, 397
399 (x,next(y),next(add(x,y)))n3
& [next(y)=1 & next(x)=next(add(x,y)) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add
& next(b')=next(y)
& next(c')=next(add(x,y))]]
Join, 398, 385
400 (x,next(y),next(add(x,y)))add
Detach, 357, 399
401 ALL(c2):ALL(d):[xn & c2n & dn => [d=add(x,c2) <=> (x,c2,d)add]]
U Spec, 291
402 ALL(d):[xn & next(y)n & dn => [d=add(x,next(y)) <=> (x,next(y),d)add]]
U Spec, 401
403 xn & next(y)n & next(add(x,y))n => [next(add(x,y))=add(x,next(y)) <=> (x,next(y),next(add(x,y)))add]
U Spec, 402
404 xn & next(y)n
Join, 350, 393
405 xn & next(y)n & next(add(x,y))n
Join, 404, 395
406 next(add(x,y))=add(x,next(y)) <=> (x,next(y),next(add(x,y)))add
Detach, 403, 405
407 [next(add(x,y))=add(x,next(y)) => (x,next(y),next(add(x,y)))add]
& [(x,next(y),next(add(x,y)))add => next(add(x,y))=add(x,next(y))]
Iff-And, 406
408 next(add(x,y))=add(x,next(y)) => (x,next(y),next(add(x,y)))add
Split, 407
409 (x,next(y),next(add(x,y)))add => next(add(x,y))=add(x,next(y))
Split, 407
410 next(add(x,y))=add(x,next(y))
Detach, 409, 400
411 add(x,next(y))=next(add(x,y))
Sym, 410
As Required:
412 xn & yn => add(x,next(y))=next(add(x,y))
Conclusion, 349
Generalizing...
413 ALL(b):[xn & bn => add(x,next(b))=next(add(x,b))]
U Gen, 412
414 ALL(a):ALL(b):[an & bn => add(a,next(b))=next(add(a,b))]
U Gen, 413
Joining results...
415 ALL(a):ALL(b):[an & bn => add(a,b)n]
& ALL(a):[an => add(a,1)=next(a)]
Join, 313, 348
416 ALL(a):ALL(b):[an & bn => add(a,b)n]
& ALL(a):[an => add(a,1)=next(a)]
& ALL(a):ALL(b):[an & bn => add(a,next(b))=next(add(a,b))]
Join, 415, 414
As Required:
417 EXIST(addn):[ALL(a):ALL(b):[an & bn => addn(a,b)n]
& ALL(a):[an => addn(a,1)=next(a)]
& ALL(a):ALL(b):[an & bn => addn(a,next(b))=next(addn(a,b))]]
E Gen, 416