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