Recursion Theorem Prove: ALL(a):ALL(b):ALL(g):[Set(a) & b ε a & ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a] => EXIST(f):[f(1)=b & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]]] Axioms ------ 1 Set(n) Axiom 2 1 ε n Axiom 3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n] Axiom 4 ALL(a):[a ε n => ~a+1=1] Axiom 5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b] Axiom 6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1] Axiom 7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]] Axiom Prove: ALL(a):ALL(b):ALL(g):[Set(a) & b ε a & ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a] => EXIST(g):[ALL(c):[c ε n => g(c) ε a] & g(1)=b & ALL(c):f(c+1)=g(c+1,f(c))]] Suppose... 8 Set(m) & m1 ε m & ALL(c):ALL(d):[c ε n & d ε m => g(c,d) ε m] Premise 9 Set(m) Split, 8 10 m1 ε m Split, 8 11 ALL(c):ALL(d):[c ε n & d ε m => g(c,d) ε m] Split, 8 Apply the Cartesian Product Axiom to construct nm (n x m) 12 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε a1 & c2 ε a2]]] Cart Prod 13 ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε a2]]] U Spec, 12 14 Set(n) & Set(m) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε m]] U Spec, 13 15 Set(n) & Set(m) Join, 1, 9 16 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε m]] Detach, 14, 15 17 Set'(nm) & ALL(c1):ALL(c2):[(c1,c2) ε nm <=> c1 ε n & c2 ε m] E Spec, 16 Define: nm (n x m) 18 Set'(nm) Split, 17 19 ALL(c1):ALL(c2):[(c1,c2) ε nm <=> c1 ε n & c2 ε m] Split, 17 Apply the Power Set Axiom to construct pnm 20 ALL(a):[Set'(a) => EXIST(b):[Set(b) & ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε a]]]] Power Set 21 Set'(nm) => EXIST(b):[Set(b) & ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]] U Spec, 20 22 EXIST(b):[Set(b) & ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]]] Detach, 21, 18 23 Set(pnm) & ALL(c):[c ε pnm <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]] E Spec, 22 Define: pnm (power set of nm) 24 Set(pnm) Split, 23 25 ALL(c):[c ε pnm <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε nm]] Split, 23 Apply the Subset Axiom to construct s 26 EXIST(sub):[Set(sub) & ALL(a):[a ε sub <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]]] Subset, 24 27 Set(s) & ALL(a):[a ε s <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]] E Spec, 26 Define: s 28 Set(s) Split, 27 29 ALL(a):[a ε s <=> a ε pnm & [(1,m1) ε a & ALL(b):ALL(c):[(b,c) ε a => (b+1,g(b+1,c)) ε a]]] Split, 27 Apply the Subset Axiom to construct f 30 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]]] Subset, 18 31 Set'(f) & ALL(a):ALL(b):[(a,b) ε f <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]] E Spec, 30 Define: f 32 Set'(f) Split, 31 33 ALL(a):ALL(b):[(a,b) ε f <=> (a,b) ε nm & ALL(c):[c ε s => (a,b) ε c]] Split, 31 34 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε a & d ε b] & ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]] Function 35 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε a & d ε b] & ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]] U Spec, 34 36 ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε b] & ALL(c):[c ε n => EXIST(d):[d ε b & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]] U Spec, 35 Sufficient: Functionality of f 37 ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m] & ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f] U Spec, 36 38 (x,y) ε f Premise 39 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 40 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 39 41 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 40 42 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 41 43 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 41 44 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 42, 38 45 (x,y) ε nm Split, 44 Functionality, Part 1 As Required: 46 ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm] Conclusion, 38 Sufficient: For Functionality, Part 2 47 EXIST(d):[d ε m & (1,d) ε f] & ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f] => EXIST(d):[d ε m & (c+1,d) ε f]] => ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] Induction 48 ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]] U Spec, 33 49 (1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] U Spec, 48 50 [(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]] & [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f] Iff-And, 49 51 (1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Split, 50 Sufficient: (1,m1) ε f 52 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f Split, 50 53 ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m] U Spec, 19 54 (1,m1) ε nm <=> 1 ε n & m1 ε m U Spec, 53 55 [(1,m1) ε nm => 1 ε n & m1 ε m] & [1 ε n & m1 ε m => (1,m1) ε nm] Iff-And, 54 56 (1,m1) ε nm => 1 ε n & m1 ε m Split, 55 57 1 ε n & m1 ε m => (1,m1) ε nm Split, 55 58 1 ε n & m1 ε m Join, 2, 10 59 (1,m1) ε nm Detach, 57, 58 Suppose... 60 t ε s Premise 61 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 62 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 61 63 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 62 64 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 62 65 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 63, 60 66 t ε pnm Split, 65 67 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 65 68 (1,m1) ε t Split, 67 69 ALL(c):[c ε s => (1,m1) ε c] Conclusion, 60 70 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Join, 59, 69 71 (1,m1) ε f Detach, 52, 70 72 m1 ε m & (1,m1) ε f Join, 10, 71 Base Case --------- As Required: 73 EXIST(d):[d ε m & (1,d) ε f] E Gen, 72 Inductive Case -------------- Suppose... 74 x ε n & EXIST(d):[d ε m & (x,d) ε f] Premise 75 x ε n Split, 74 76 EXIST(d):[d ε m & (x,d) ε f] Split, 74 77 y ε m & (x,y) ε f E Spec, 76 Define: y 78 y ε m Split, 77 79 (x,y) ε f Split, 77 80 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 81 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 80 82 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 81 83 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 82 84 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 82 85 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 83, 79 86 (x,y) ε nm Split, 85 87 ALL(c):[c ε s => (x,y) ε c] Split, 85 88 ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]] U Spec, 33 89 (x+1,g(x+1,y)) ε f <=> (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] U Spec, 88 90 [(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]] & [(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f] Iff-And, 89 91 (x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Split, 90 Sufficient: (x+1,g(x+1,y)) ε f 92 (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f Split, 90 93 ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m] U Spec, 19 94 (x+1,g(x+1,y)) ε nm <=> x+1 ε n & g(x+1,y) ε m U Spec, 93 95 [(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m] & [x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm] Iff-And, 94 96 (x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m Split, 95 97 x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm Split, 95 98 ALL(b):[x ε n & b ε n => x+b ε n] U Spec, 3 99 x ε n & 1 ε n => x+1 ε n U Spec, 98 100 x ε n & 1 ε n Join, 75, 2 101 x+1 ε n Detach, 99, 100 102 ALL(d):[x+1 ε n & d ε m => g(x+1,d) ε m] U Spec, 11 103 x+1 ε n & y ε m => g(x+1,y) ε m U Spec, 102 104 x+1 ε n & y ε m Join, 101, 78 105 g(x+1,y) ε m Detach, 103, 104 106 x+1 ε n & g(x+1,y) ε m Join, 101, 105 107 (x+1,g(x+1,y)) ε nm Detach, 97, 106 Supppose... 108 t ε s Premise 109 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 110 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 109 111 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 110 112 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 110 113 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 111, 108 114 t ε pnm Split, 113 115 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 113 116 (1,m1) ε t Split, 115 117 ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 115 118 ALL(c):[(x,c) ε t => (x+1,g(x+1,c)) ε t] U Spec, 117 119 (x,y) ε t => (x+1,g(x+1,y)) ε t U Spec, 118 120 t ε s => (x,y) ε t U Spec, 87 121 (x,y) ε t Detach, 120, 108 122 (x+1,g(x+1,y)) ε t Detach, 119, 121 123 ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Conclusion, 108 124 (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Join, 107, 123 125 (x+1,g(x+1,y)) ε f Detach, 92, 124 126 g(x+1,y) ε m & (x+1,g(x+1,y)) ε f Join, 105, 125 127 EXIST(d):[d ε m & (x+1,d) ε f] E Gen, 126 Inductive Case -------------- As Required: 128 ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f] => EXIST(d):[d ε m & (c+1,d) ε f]] Conclusion, 74 129 EXIST(d):[d ε m & (1,d) ε f] & ALL(c):[c ε n & EXIST(d):[d ε m & (c,d) ε f] => EXIST(d):[d ε m & (c+1,d) ε f]] Join, 73, 128 Functionality, Part 2 As Required: 130 ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] Detach, 47, 129 Sufficient: For Functionality, Part 3 131 ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2] & ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]] => ALL(c):[c ε n => ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]] Induction Suppose to contrary... 132 (1,y) ε f & ~y=m1 Premise 133 (1,y) ε f Split, 132 134 ~y=m1 Split, 132 135 ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]] U Spec, 33 136 (1,y) ε f <=> (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] U Spec, 135 137 [(1,y) ε f => (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c]] & [(1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] => (1,y) ε f] Iff-And, 136 138 (1,y) ε f => (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] Split, 137 139 (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] => (1,y) ε f Split, 137 140 (1,y) ε nm & ALL(c):[c ε s => (1,y) ε c] Detach, 138, 133 141 (1,y) ε nm Split, 140 142 ALL(c):[c ε s => (1,y) ε c] Split, 140 143 ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m] U Spec, 19 144 (1,y) ε nm <=> 1 ε n & y ε m U Spec, 143 145 [(1,y) ε nm => 1 ε n & y ε m] & [1 ε n & y ε m => (1,y) ε nm] Iff-And, 144 146 (1,y) ε nm => 1 ε n & y ε m Split, 145 147 1 ε n & y ε m => (1,y) ε nm Split, 145 148 1 ε n & y ε m Detach, 146, 141 149 1 ε n Split, 148 150 y ε m Split, 148 151 ~EXIST(c):~[c ε s => (1,y) ε c] Quant, 142 152 ~EXIST(c):~~[c ε s & ~(1,y) ε c] Imply-And, 151 Obtain a contradiction by constructing a subset f' of n2 that excludes (1,y) and is an element of s. 153 ~EXIST(c):[c ε s & ~(1,y) ε c] Rem DNeg, 152 154 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε nm & ~[a=1 & b=y]]] Subset, 18 155 Set'(f') & ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε nm & ~[a=1 & b=y]] E Spec, 154 Define: f' Prove: f' ε s 156 Set'(f') Split, 155 157 ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε nm & ~[a=1 & b=y]] Split, 155 158 f' ε s <=> f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] U Spec, 29 159 [f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]] & [f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s] Iff-And, 158 160 f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] Split, 159 Sufficient: f' ε s 161 f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s Split, 159 162 f' ε pnm <=> Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] U Spec, 25 163 [f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]] & [Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm] Iff-And, 162 164 f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Split, 163 Sufficient: f' ε pnm 165 Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm Split, 163 Suppose... 166 (p,q) ε f' Premise 167 ALL(b):[(p,b) ε f' <=> (p,b) ε nm & ~[p=1 & b=y]] U Spec, 157 168 (p,q) ε f' <=> (p,q) ε nm & ~[p=1 & q=y] U Spec, 167 169 [(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]] & [(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f'] Iff-And, 168 170 (p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y] Split, 169 171 (p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f' Split, 169 172 (p,q) ε nm & ~[p=1 & q=y] Detach, 170, 166 173 (p,q) ε nm Split, 172 174 ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Conclusion, 166 175 Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Join, 156, 174 176 f' ε pnm Detach, 165, 175 177 ALL(b):[(1,b) ε f' <=> (1,b) ε nm & ~[1=1 & b=y]] U Spec, 157 178 (1,m1) ε f' <=> (1,m1) ε nm & ~[1=1 & m1=y] U Spec, 177 179 [(1,m1) ε f' => (1,m1) ε nm & ~[1=1 & m1=y]] & [(1,m1) ε nm & ~[1=1 & m1=y] => (1,m1) ε f'] Iff-And, 178 180 (1,m1) ε f' => (1,m1) ε nm & ~[1=1 & m1=y] Split, 179 181 (1,m1) ε nm & ~[1=1 & m1=y] => (1,m1) ε f' Split, 179 182 (1,m1) ε nm & ~~[~1=1 | ~m1=y] => (1,m1) ε f' DeMorgan, 181 Sufficient: (1,m1) ε f' 183 (1,m1) ε nm & [~1=1 | ~m1=y] => (1,m1) ε f' Rem DNeg, 182 184 ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m] U Spec, 19 185 (1,m1) ε nm <=> 1 ε n & m1 ε m U Spec, 184 186 [(1,m1) ε nm => 1 ε n & m1 ε m] & [1 ε n & m1 ε m => (1,m1) ε nm] Iff-And, 185 187 (1,m1) ε nm => 1 ε n & m1 ε m Split, 186 188 1 ε n & m1 ε m => (1,m1) ε nm Split, 186 189 1 ε n & m1 ε m Join, 2, 10 190 (1,m1) ε nm Detach, 188, 189 191 ~m1=y Sym, 134 192 ~1=1 | ~m1=y Arb Or, 191 193 (1,m1) ε nm & [~1=1 | ~m1=y] Join, 190, 192 194 (1,m1) ε f' Detach, 183, 193 Suppose... 195 (p,q) ε f' Premise 196 ALL(b):[(p,b) ε f' <=> (p,b) ε nm & ~[p=1 & b=y]] U Spec, 157 197 (p,q) ε f' <=> (p,q) ε nm & ~[p=1 & q=y] U Spec, 196 198 [(p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y]] & [(p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f'] Iff-And, 197 199 (p,q) ε f' => (p,q) ε nm & ~[p=1 & q=y] Split, 198 200 (p,q) ε nm & ~[p=1 & q=y] => (p,q) ε f' Split, 198 201 (p,q) ε nm & ~[p=1 & q=y] Detach, 199, 195 202 (p,q) ε nm Split, 201 203 ~[p=1 & q=y] Split, 201 204 ALL(c2):[(p,c2) ε nm <=> p ε n & c2 ε m] U Spec, 19 205 (p,q) ε nm <=> p ε n & q ε m U Spec, 204 206 [(p,q) ε nm => p ε n & q ε m] & [p ε n & q ε m => (p,q) ε nm] Iff-And, 205 207 (p,q) ε nm => p ε n & q ε m Split, 206 208 p ε n & q ε m => (p,q) ε nm Split, 206 209 p ε n & q ε m Detach, 207, 202 210 p ε n Split, 209 211 q ε m Split, 209 212 ALL(b):[(p+1,b) ε f' <=> (p+1,b) ε nm & ~[p+1=1 & b=y]] U Spec, 157 213 (p+1,g(p+1,q)) ε f' <=> (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] U Spec, 212 214 [(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y]] & [(p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] => (p+1,g(p+1,q)) ε f'] Iff-And, 213 215 (p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] Split, 214 216 (p+1,g(p+1,q)) ε nm & ~[p+1=1 & g(p+1,q)=y] => (p+1,g(p+1,q)) ε f' Split, 214 217 (p+1,g(p+1,q)) ε nm & ~~[~p+1=1 | ~g(p+1,q)=y] => (p+1,g(p+1,q)) ε f' DeMorgan, 216 Sufficient: (p+1,g(p+1,q)) ε f' 218 (p+1,g(p+1,q)) ε nm & [~p+1=1 | ~g(p+1,q)=y] => (p+1,g(p+1,q)) ε f' Rem DNeg, 217 219 ALL(c2):[(p+1,c2) ε nm <=> p+1 ε n & c2 ε m] U Spec, 19 220 (p+1,g(p+1,q)) ε nm <=> p+1 ε n & g(p+1,q) ε m U Spec, 219 221 [(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m] & [p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm] Iff-And, 220 222 (p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m Split, 221 Sufficient: (p+1,g(p+1,q)) ε nm 223 p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm Split, 221 224 ALL(b):[p ε n & b ε n => p+b ε n] U Spec, 3 225 p ε n & 1 ε n => p+1 ε n U Spec, 224 226 p ε n & 1 ε n Join, 210, 2 227 p+1 ε n Detach, 225, 226 228 ALL(d):[p+1 ε n & d ε m => g(p+1,d) ε m] U Spec, 11 229 p+1 ε n & q ε m => g(p+1,q) ε m U Spec, 228 230 p+1 ε n & q ε m Join, 227, 211 231 g(p+1,q) ε m Detach, 229, 230 232 p+1 ε n & g(p+1,q) ε m Join, 227, 231 233 (p+1,g(p+1,q)) ε nm Detach, 223, 232 234 p ε n => ~p+1=1 U Spec, 4 235 ~p+1=1 Detach, 234, 210 236 ~p+1=1 | ~g(p+1,q)=y Arb Or, 235 237 (p+1,g(p+1,q)) ε nm & [~p+1=1 | ~g(p+1,q)=y] Join, 233, 236 238 (p+1,g(p+1,q)) ε f' Detach, 218, 237 239 ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f'] Conclusion, 195 240 (1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f'] Join, 194, 239 241 f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] Join, 176, 240 242 f' ε s Detach, 161, 241 243 ALL(b):[(1,b) ε f' <=> (1,b) ε nm & ~[1=1 & b=y]] U Spec, 157 244 (1,y) ε f' <=> (1,y) ε nm & ~[1=1 & y=y] U Spec, 243 245 [(1,y) ε f' => (1,y) ε nm & ~[1=1 & y=y]] & [(1,y) ε nm & ~[1=1 & y=y] => (1,y) ε f'] Iff-And, 244 246 (1,y) ε f' => (1,y) ε nm & ~[1=1 & y=y] Split, 245 247 (1,y) ε nm & ~[1=1 & y=y] => (1,y) ε f' Split, 245 Sufficient: ~(1,y) ε f' (line 332 in factorial.proof) 248 ~[(1,y) ε nm & ~[1=1 & y=y]] => ~(1,y) ε f' Contra, 246 249 ~~[~(1,y) ε nm | ~~[1=1 & y=y]] => ~(1,y) ε f' DeMorgan, 248 250 ~(1,y) ε nm | ~~[1=1 & y=y] => ~(1,y) ε f' Rem DNeg, 249 251 ~(1,y) ε nm | 1=1 & y=y => ~(1,y) ε f' Rem DNeg, 250 252 1=1 Reflex 253 y=y Reflex 254 1=1 & y=y Join, 252, 253 255 ~(1,y) ε nm | 1=1 & y=y Arb Or, 254 256 ~(1,y) ε f' Detach, 251, 255 257 f' ε s & ~(1,y) ε f' Join, 242, 256 258 EXIST(c):[c ε s & ~(1,y) ε c] E Gen, 257 259 EXIST(c):[c ε s & ~(1,y) ε c] & ~EXIST(c):[c ε s & ~(1,y) ε c] Join, 258, 153 260 ALL(b):~[(1,b) ε f & ~b=m1] Conclusion, 132 261 ALL(b):~~[(1,b) ε f => ~~b=m1] Imply-And, 260 262 ALL(b):[(1,b) ε f => ~~b=m1] Rem DNeg, 261 263 ALL(b):[(1,b) ε f => b=m1] Rem DNeg, 262 Suppose... 264 (1,y) ε f & (1,y') ε f Premise 265 (1,y) ε f Split, 264 266 (1,y') ε f Split, 264 267 (1,y) ε f => y=m1 U Spec, 263 268 y=m1 Detach, 267, 265 269 (1,y') ε f => y'=m1 U Spec, 263 270 y'=m1 Detach, 269, 266 271 y=y' Substitute, 270, 268 Base Step --------- As Required: 272 ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2] Conclusion, 264 Inductive Step -------------- Suppose... 273 x ε n & ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2] Premise 274 x ε n Split, 273 275 ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2] Split, 273 Prove: ALL(a):[(x,a) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,a)]] (line 357 of factorial.proof) Suppose... 276 (x,y) ε f Premise 277 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 278 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 277 279 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 278 280 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 279 281 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 279 282 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 280, 276 283 (x,y) ε nm Split, 282 284 ALL(c):[c ε s => (x,y) ε c] Split, 282 285 ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m] U Spec, 19 286 (x,y) ε nm <=> x ε n & y ε m U Spec, 285 287 [(x,y) ε nm => x ε n & y ε m] & [x ε n & y ε m => (x,y) ε nm] Iff-And, 286 288 (x,y) ε nm => x ε n & y ε m Split, 287 289 x ε n & y ε m => (x,y) ε nm Split, 287 290 x ε n & y ε m Detach, 288, 283 291 x ε n Split, 290 292 y ε m Split, 290 Suppose... 293 (x+1,y') ε f & ~y'=g(x+1,y) Premise 294 (x+1,y') ε f Split, 293 295 ~y'=g(x+1,y) Split, 293 296 ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]] U Spec, 33 297 (x+1,y') ε f <=> (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] U Spec, 296 298 [(x+1,y') ε f => (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c]] & [(x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] => (x+1,y') ε f] Iff-And, 297 299 (x+1,y') ε f => (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] Split, 298 300 (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] => (x+1,y') ε f Split, 298 301 (x+1,y') ε nm & ALL(c):[c ε s => (x+1,y') ε c] Detach, 299, 294 302 (x+1,y') ε nm Split, 301 303 ALL(c):[c ε s => (x+1,y') ε c] Split, 301 304 ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m] U Spec, 19 305 (x+1,y') ε nm <=> x+1 ε n & y' ε m U Spec, 304 306 [(x+1,y') ε nm => x+1 ε n & y' ε m] & [x+1 ε n & y' ε m => (x+1,y') ε nm] Iff-And, 305 307 (x+1,y') ε nm => x+1 ε n & y' ε m Split, 306 308 x+1 ε n & y' ε m => (x+1,y') ε nm Split, 306 309 x+1 ε n & y' ε m Detach, 307, 302 310 x+1 ε n Split, 309 311 y' ε m Split, 309 312 ~EXIST(c):~[c ε s => (x+1,y') ε c] Quant, 303 313 ~EXIST(c):~~[c ε s & ~(x+1,y') ε c] Imply-And, 312 Obtain a contradiction by proving to the contrary that EXIST(c):[c ε s & ~(x+1,y') ε c] 314 ~EXIST(c):[c ε s & ~(x+1,y') ε c] Rem DNeg, 313 315 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε f & ~[a=x+1 & b=y']]] Subset, 32 316 Set'(f') & ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε f & ~[a=x+1 & b=y']] E Spec, 315 Define: f' Prove: f' ε s 317 Set'(f') Split, 316 318 ALL(a):ALL(b):[(a,b) ε f' <=> (a,b) ε f & ~[a=x+1 & b=y']] Split, 316 319 f' ε s <=> f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] U Spec, 29 320 [f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']]] & [f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s] Iff-And, 319 321 f' ε s => f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] Split, 320 Sufficient: f' ε s 322 f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] => f' ε s Split, 320 323 f' ε pnm <=> Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] U Spec, 25 324 [f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm]] & [Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm] Iff-And, 323 325 f' ε pnm => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Split, 324 Sufficient: f' ε pnm 326 Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] => f' ε pnm Split, 324 Suppose... 327 (p,q) ε f' Premise 328 ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']] U Spec, 318 329 (p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y'] U Spec, 328 330 [(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']] & [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'] Iff-And, 329 331 (p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y'] Split, 330 332 (p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f' Split, 330 333 (p,q) ε f & ~[p=x+1 & q=y'] Detach, 331, 327 334 (p,q) ε f Split, 333 335 ~[p=x+1 & q=y'] Split, 333 336 ALL(b):[(p,b) ε f <=> (p,b) ε nm & ALL(c):[c ε s => (p,b) ε c]] U Spec, 33 337 (p,q) ε f <=> (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] U Spec, 336 338 [(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]] & [(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f] Iff-And, 337 339 (p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] Split, 338 340 (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f Split, 338 341 (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] Detach, 339, 334 342 (p,q) ε nm Split, 341 343 ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Conclusion, 327 344 Set'(f') & ALL(d1):ALL(d2):[(d1,d2) ε f' => (d1,d2) ε nm] Join, 317, 343 345 f' ε pnm Detach, 326, 344 346 ALL(b):[(1,b) ε f' <=> (1,b) ε f & ~[1=x+1 & b=y']] U Spec, 318 347 (1,m1) ε f' <=> (1,m1) ε f & ~[1=x+1 & m1=y'] U Spec, 346 348 [(1,m1) ε f' => (1,m1) ε f & ~[1=x+1 & m1=y']] & [(1,m1) ε f & ~[1=x+1 & m1=y'] => (1,m1) ε f'] Iff-And, 347 349 (1,m1) ε f' => (1,m1) ε f & ~[1=x+1 & m1=y'] Split, 348 350 (1,m1) ε f & ~[1=x+1 & m1=y'] => (1,m1) ε f' Split, 348 351 (1,m1) ε f & ~~[~1=x+1 | ~m1=y'] => (1,m1) ε f' DeMorgan, 350 Sufficient: (1,m1) ε f' 352 (1,m1) ε f & [~1=x+1 | ~m1=y'] => (1,m1) ε f' Rem DNeg, 351 353 ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]] U Spec, 33 354 (1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] U Spec, 353 355 [(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]] & [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f] Iff-And, 354 356 (1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Split, 355 Sufficient: (1,m1) ε f 357 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f Split, 355 358 ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m] U Spec, 19 359 (1,m1) ε nm <=> 1 ε n & m1 ε m U Spec, 358 360 [(1,m1) ε nm => 1 ε n & m1 ε m] & [1 ε n & m1 ε m => (1,m1) ε nm] Iff-And, 359 361 (1,m1) ε nm => 1 ε n & m1 ε m Split, 360 362 1 ε n & m1 ε m => (1,m1) ε nm Split, 360 363 1 ε n & m1 ε m Join, 2, 10 364 (1,m1) ε nm Detach, 362, 363 365 t ε s Premise 366 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 367 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 366 368 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 367 369 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 367 370 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 368, 365 371 t ε pnm Split, 370 372 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 370 373 (1,m1) ε t Split, 372 374 ALL(c):[c ε s => (1,m1) ε c] Conclusion, 365 375 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Join, 364, 374 376 (1,m1) ε f Detach, 357, 375 377 x ε n => ~x+1=1 U Spec, 4 378 ~x+1=1 Detach, 377, 274 379 ~1=x+1 Sym, 378 380 ~1=x+1 | ~m1=y' Arb Or, 379 381 (1,m1) ε f & [~1=x+1 | ~m1=y'] Join, 376, 380 382 (1,m1) ε f' Detach, 352, 381 383 (p,q) ε f' Premise 384 ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']] U Spec, 318 385 (p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y'] U Spec, 384 386 [(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']] & [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'] Iff-And, 385 387 (p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y'] Split, 386 388 (p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f' Split, 386 389 (p,q) ε f & ~[p=x+1 & q=y'] Detach, 387, 383 390 (p,q) ε f Split, 389 391 ~[p=x+1 & q=y'] Split, 389 392 ALL(b):[(p,b) ε f <=> (p,b) ε nm & ALL(c):[c ε s => (p,b) ε c]] U Spec, 33 393 (p,q) ε f <=> (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] U Spec, 392 394 [(p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c]] & [(p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f] Iff-And, 393 395 (p,q) ε f => (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] Split, 394 396 (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] => (p,q) ε f Split, 394 397 (p,q) ε nm & ALL(c):[c ε s => (p,q) ε c] Detach, 395, 390 398 (p,q) ε nm Split, 397 399 ALL(c):[c ε s => (p,q) ε c] Split, 397 400 ALL(c2):[(p,c2) ε nm <=> p ε n & c2 ε m] U Spec, 19 401 (p,q) ε nm <=> p ε n & q ε m U Spec, 400 402 [(p,q) ε nm => p ε n & q ε m] & [p ε n & q ε m => (p,q) ε nm] Iff-And, 401 403 (p,q) ε nm => p ε n & q ε m Split, 402 404 p ε n & q ε m => (p,q) ε nm Split, 402 405 p ε n & q ε m Detach, 403, 398 406 p ε n Split, 405 407 q ε m Split, 405 408 ALL(b):[(p,b) ε f' <=> (p,b) ε f & ~[p=x+1 & b=y']] U Spec, 318 409 (p,q) ε f' <=> (p,q) ε f & ~[p=x+1 & q=y'] U Spec, 408 410 [(p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y']] & [(p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f'] Iff-And, 409 411 (p,q) ε f' => (p,q) ε f & ~[p=x+1 & q=y'] Split, 410 412 (p,q) ε f & ~[p=x+1 & q=y'] => (p,q) ε f' Split, 410 413 (p,q) ε f & ~[p=x+1 & q=y'] Detach, 411, 383 414 (p,q) ε f Split, 413 415 ~[p=x+1 & q=y'] Split, 413 416 ALL(b):[(p+1,b) ε f' <=> (p+1,b) ε f & ~[p+1=x+1 & b=y']] U Spec, 318 417 (p+1,g(p+1,q)) ε f' <=> (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] U Spec, 416 418 [(p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y']] & [(p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] => (p+1,g(p+1,q)) ε f'] Iff-And, 417 419 (p+1,g(p+1,q)) ε f' => (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] Split, 418 Sufficient: (p+1,g(p+1,q)) ε f' 420 (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] => (p+1,g(p+1,q)) ε f' Split, 418 421 ALL(b):[(p+1,b) ε f <=> (p+1,b) ε nm & ALL(c):[c ε s => (p+1,b) ε c]] U Spec, 33 422 (p+1,g(p+1,q)) ε f <=> (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] U Spec, 421 423 [(p+1,g(p+1,q)) ε f => (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c]] & [(p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] => (p+1,g(p+1,q)) ε f] Iff-And, 422 424 (p+1,g(p+1,q)) ε f => (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] Split, 423 Sufficient: (p+1,g(p+1,q)) ε f 425 (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] => (p+1,g(p+1,q)) ε f Split, 423 426 ALL(c2):[(p+1,c2) ε nm <=> p+1 ε n & c2 ε m] U Spec, 19 427 (p+1,g(p+1,q)) ε nm <=> p+1 ε n & g(p+1,q) ε m U Spec, 426 428 [(p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m] & [p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm] Iff-And, 427 429 (p+1,g(p+1,q)) ε nm => p+1 ε n & g(p+1,q) ε m Split, 428 430 p+1 ε n & g(p+1,q) ε m => (p+1,g(p+1,q)) ε nm Split, 428 431 ALL(d):[p+1 ε n & d ε m => g(p+1,d) ε m] U Spec, 11 432 p+1 ε n & q ε m => g(p+1,q) ε m U Spec, 431 433 ALL(b):[p ε n & b ε n => p+b ε n] U Spec, 3 434 p ε n & 1 ε n => p+1 ε n U Spec, 433 435 p ε n & 1 ε n Join, 406, 2 436 p+1 ε n Detach, 434, 435 437 p+1 ε n & q ε m Join, 436, 407 438 g(p+1,q) ε m Detach, 432, 437 439 p+1 ε n & g(p+1,q) ε m Join, 436, 438 440 (p+1,g(p+1,q)) ε nm Detach, 430, 439 Suppose... 441 t ε s Premise 442 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 443 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 442 444 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 443 445 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 443 446 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 444, 441 447 t ε pnm Split, 446 448 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 446 449 (1,m1) ε t Split, 448 450 ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 448 451 ALL(c):[(p,c) ε t => (p+1,g(p+1,c)) ε t] U Spec, 450 452 (p,q) ε t => (p+1,g(p+1,q)) ε t U Spec, 451 453 t ε s => (p,q) ε t U Spec, 399 454 (p,q) ε t Detach, 453, 441 455 (p+1,g(p+1,q)) ε t Detach, 452, 454 456 ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] Conclusion, 441 457 (p+1,g(p+1,q)) ε nm & ALL(c):[c ε s => (p+1,g(p+1,q)) ε c] Join, 440, 456 458 (p+1,g(p+1,q)) ε f Detach, 425, 457 459 p+1=x+1 Premise 460 ALL(b):[p ε n & b ε n & p+1=b+1 => p=b] U Spec, 5 461 p ε n & x ε n & p+1=x+1 => p=x U Spec, 460 462 p ε n & x ε n Join, 406, 274 463 p ε n & x ε n & p+1=x+1 Join, 462, 459 464 p=x Detach, 461, 463 465 (x,q) ε f Substitute, 464, 414 466 ALL(d2):[(x,q) ε f & (x,d2) ε f => q=d2] U Spec, 275 467 (x,q) ε f & (x,y) ε f => q=y U Spec, 466 468 (x,q) ε f & (x,y) ε f Join, 465, 276 469 q=y Detach, 467, 468 470 ~y'=g(x+1,q) Substitute, 469, 295 471 ~y'=g(p+1,q) Substitute, 464, 470 472 ~g(p+1,q)=y' Sym, 471 473 p+1=x+1 => ~g(p+1,q)=y' Conclusion, 459 474 ~[p+1=x+1 & ~~g(p+1,q)=y'] Imply-And, 473 475 ~[p+1=x+1 & g(p+1,q)=y'] Rem DNeg, 474 476 (p+1,g(p+1,q)) ε f & ~[p+1=x+1 & g(p+1,q)=y'] Join, 458, 475 477 (p+1,g(p+1,q)) ε f' Detach, 420, 476 478 ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f'] Conclusion, 383 479 (1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f'] Join, 382, 478 480 f' ε pnm & [(1,m1) ε f' & ALL(b):ALL(c):[(b,c) ε f' => (b+1,g(b+1,c)) ε f']] Join, 345, 479 line 546 in factorial.proof 481 f' ε s Detach, 322, 480 482 ALL(b):[(x+1,b) ε f' <=> (x+1,b) ε f & ~[x+1=x+1 & b=y']] U Spec, 318 483 (x+1,y') ε f' <=> (x+1,y') ε f & ~[x+1=x+1 & y'=y'] U Spec, 482 484 [(x+1,y') ε f' => (x+1,y') ε f & ~[x+1=x+1 & y'=y']] & [(x+1,y') ε f & ~[x+1=x+1 & y'=y'] => (x+1,y') ε f'] Iff-And, 483 485 (x+1,y') ε f' => (x+1,y') ε f & ~[x+1=x+1 & y'=y'] Split, 484 486 (x+1,y') ε f & ~[x+1=x+1 & y'=y'] => (x+1,y') ε f' Split, 484 Sufficient: ~(x+1,y') ε f' 487 ~[(x+1,y') ε f & ~[x+1=x+1 & y'=y']] => ~(x+1,y') ε f' Contra, 485 488 ~~[~(x+1,y') ε f | ~~[x+1=x+1 & y'=y']] => ~(x+1,y') ε f' DeMorgan, 487 489 ~(x+1,y') ε f | ~~[x+1=x+1 & y'=y'] => ~(x+1,y') ε f' Rem DNeg, 488 490 ~(x+1,y') ε f | x+1=x+1 & y'=y' => ~(x+1,y') ε f' Rem DNeg, 489 491 x+1=x+1 Reflex 492 y'=y' Reflex 493 x+1=x+1 & y'=y' Join, 491, 492 494 ~(x+1,y') ε f | x+1=x+1 & y'=y' Arb Or, 493 495 ~(x+1,y') ε f' Detach, 490, 494 496 f' ε s & ~(x+1,y') ε f' Join, 481, 495 497 EXIST(c):[c ε s & ~(x+1,y') ε c] E Gen, 496 498 EXIST(c):[c ε s & ~(x+1,y') ε c] & ~EXIST(c):[c ε s & ~(x+1,y') ε c] Join, 497, 314 499 ALL(b):~[(x+1,b) ε f & ~b=g(x+1,y)] Conclusion, 293 500 ALL(b):~~[(x+1,b) ε f => ~~b=g(x+1,y)] Imply-And, 499 501 ALL(b):[(x+1,b) ε f => ~~b=g(x+1,y)] Rem DNeg, 500 502 ALL(b):[(x+1,b) ε f => b=g(x+1,y)] Rem DNeg, 501 503 ALL(a):[(x,a) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,a)]] Conclusion, 276 504 x ε n => EXIST(d):[d ε m & (x,d) ε f] U Spec, 130 505 EXIST(d):[d ε m & (x,d) ε f] Detach, 504, 274 506 y ε m & (x,y) ε f E Spec, 505 Define: y 507 y ε m Split, 506 508 (x,y) ε f Split, 506 509 (x,y) ε f => ALL(b):[(x+1,b) ε f => b=g(x+1,y)] U Spec, 503 510 ALL(b):[(x+1,b) ε f => b=g(x+1,y)] Detach, 509, 508 Suppose... 511 (x+1,y') ε f & (x+1,y'') ε f Premise 512 (x+1,y') ε f Split, 511 513 (x+1,y'') ε f Split, 511 514 (x+1,y') ε f => y'=g(x+1,y) U Spec, 510 515 y'=g(x+1,y) Detach, 514, 512 516 (x+1,y'') ε f => y''=g(x+1,y) U Spec, 510 517 y''=g(x+1,y) Detach, 516, 513 518 y'=y'' Substitute, 517, 515 519 ALL(d1):ALL(d2):[(x+1,d1) ε f & (x+1,d2) ε f => d1=d2] Conclusion, 511 Inductive Step -------------- As Required: 520 ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]] Conclusion, 273 521 ALL(d1):ALL(d2):[(1,d1) ε f & (1,d2) ε f => d1=d2] & ALL(c):[c ε n & ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] => ALL(d1):ALL(d2):[(c+1,d1) ε f & (c+1,d2) ε f => d1=d2]] Join, 272, 520 By induction... 522 ALL(c):[c ε n => ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]] Detach, 131, 521 Suppose... 523 (x,y) ε f & (x,y') ε f Premise 524 (x,y) ε f Split, 523 525 (x,y') ε f Split, 523 526 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 527 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 526 528 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 527 529 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 528 530 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 528 531 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 529, 524 532 (x,y) ε nm Split, 531 533 ALL(c):[c ε s => (x,y) ε c] Split, 531 534 ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m] U Spec, 19 535 (x,y) ε nm <=> x ε n & y ε m U Spec, 534 536 [(x,y) ε nm => x ε n & y ε m] & [x ε n & y ε m => (x,y) ε nm] Iff-And, 535 537 (x,y) ε nm => x ε n & y ε m Split, 536 538 x ε n & y ε m => (x,y) ε nm Split, 536 539 x ε n & y ε m Detach, 537, 532 540 x ε n Split, 539 541 y ε m Split, 539 542 x ε n => ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2] U Spec, 522 543 ALL(d1):ALL(d2):[(x,d1) ε f & (x,d2) ε f => d1=d2] Detach, 542, 540 544 ALL(d2):[(x,y) ε f & (x,d2) ε f => y=d2] U Spec, 543 545 (x,y) ε f & (x,y') ε f => y=y' U Spec, 544 546 (x,y) ε f & (x,y') ε f Join, 524, 525 547 y=y' Detach, 545, 546 Functionality, Part 3 As Required: 548 ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] Conclusion, 523 549 ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm] & ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] Join, 46, 130 550 ALL(c):ALL(d):[(c,d) ε f => (c,d) ε nm] & ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] Join, 549, 548 551 (x,y) ε f Premise 552 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 553 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 552 554 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 553 555 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 554 556 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 554 557 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 555, 551 558 (x,y) ε nm Split, 557 559 ALL(c):[c ε s => (x,y) ε c] Split, 557 560 ALL(c2):[(x,c2) ε nm <=> x ε n & c2 ε m] U Spec, 19 561 (x,y) ε nm <=> x ε n & y ε m U Spec, 560 562 [(x,y) ε nm => x ε n & y ε m] & [x ε n & y ε m => (x,y) ε nm] Iff-And, 561 563 (x,y) ε nm => x ε n & y ε m Split, 562 564 x ε n & y ε m => (x,y) ε nm Split, 562 565 x ε n & y ε m Detach, 563, 558 Functionality, Part 1 566 ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m] Conclusion, 551 567 ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m] & ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] Join, 566, 130 568 ALL(c):ALL(d):[(c,d) ε f => c ε n & d ε m] & ALL(c):[c ε n => EXIST(d):[d ε m & (c,d) ε f]] & ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2] Join, 567, 548 f is a function 569 ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f] Detach, 37, 568 570 ALL(d):[d=f(1) <=> (1,d) ε f] U Spec, 569 571 m1=f(1) <=> (1,m1) ε f U Spec, 570 572 [m1=f(1) => (1,m1) ε f] & [(1,m1) ε f => m1=f(1)] Iff-And, 571 573 m1=f(1) => (1,m1) ε f Split, 572 574 (1,m1) ε f => m1=f(1) Split, 572 575 ALL(b):[(1,b) ε f <=> (1,b) ε nm & ALL(c):[c ε s => (1,b) ε c]] U Spec, 33 576 (1,m1) ε f <=> (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] U Spec, 575 577 [(1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c]] & [(1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f] Iff-And, 576 578 (1,m1) ε f => (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Split, 577 Sufficient: (1,m1) ε f 579 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] => (1,m1) ε f Split, 577 580 ALL(c2):[(1,c2) ε nm <=> 1 ε n & c2 ε m] U Spec, 19 581 (1,m1) ε nm <=> 1 ε n & m1 ε m U Spec, 580 582 [(1,m1) ε nm => 1 ε n & m1 ε m] & [1 ε n & m1 ε m => (1,m1) ε nm] Iff-And, 581 583 (1,m1) ε nm => 1 ε n & m1 ε m Split, 582 584 1 ε n & m1 ε m => (1,m1) ε nm Split, 582 585 1 ε n & m1 ε m Join, 2, 10 586 (1,m1) ε nm Detach, 584, 585 587 t ε s Premise 588 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 589 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 588 590 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 589 591 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 589 592 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 590, 587 593 t ε pnm Split, 592 594 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 592 595 (1,m1) ε t Split, 594 596 ALL(c):[c ε s => (1,m1) ε c] Conclusion, 587 597 (1,m1) ε nm & ALL(c):[c ε s => (1,m1) ε c] Join, 586, 596 598 (1,m1) ε f Detach, 579, 597 599 m1=f(1) Detach, 574, 598 600 f(1)=m1 Sym, 599 Prove: ALL(a):[a ε n => f(a+1)=g(a+1,f(a))] Suppose... 601 x ε n Premise 602 x ε n => EXIST(d):[d ε m & (x,d) ε f] U Spec, 130 603 EXIST(d):[d ε m & (x,d) ε f] Detach, 602, 601 604 y ε m & (x,y) ε f E Spec, 603 Define: y 605 y ε m Split, 604 606 (x,y) ε f Split, 604 607 ALL(b):[(x,b) ε f <=> (x,b) ε nm & ALL(c):[c ε s => (x,b) ε c]] U Spec, 33 608 (x,y) ε f <=> (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] U Spec, 607 609 [(x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c]] & [(x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f] Iff-And, 608 610 (x,y) ε f => (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Split, 609 611 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] => (x,y) ε f Split, 609 612 (x,y) ε nm & ALL(c):[c ε s => (x,y) ε c] Detach, 610, 606 613 (x,y) ε nm Split, 612 614 ALL(c):[c ε s => (x,y) ε c] Split, 612 615 ALL(b):[(x+1,b) ε f <=> (x+1,b) ε nm & ALL(c):[c ε s => (x+1,b) ε c]] U Spec, 33 616 (x+1,g(x+1,y)) ε f <=> (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] U Spec, 615 617 [(x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c]] & [(x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f] Iff-And, 616 618 (x+1,g(x+1,y)) ε f => (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Split, 617 Sufficient: (x+1,g(x+1,y)) ε f 619 (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] => (x+1,g(x+1,y)) ε f Split, 617 620 ALL(c2):[(x+1,c2) ε nm <=> x+1 ε n & c2 ε m] U Spec, 19 621 (x+1,g(x+1,y)) ε nm <=> x+1 ε n & g(x+1,y) ε m U Spec, 620 622 [(x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m] & [x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm] Iff-And, 621 623 (x+1,g(x+1,y)) ε nm => x+1 ε n & g(x+1,y) ε m Split, 622 Sufficient: (x+1,g(x+1,y)) ε nm 624 x+1 ε n & g(x+1,y) ε m => (x+1,g(x+1,y)) ε nm Split, 622 625 ALL(b):[x ε n & b ε n => x+b ε n] U Spec, 3 626 x ε n & 1 ε n => x+1 ε n U Spec, 625 627 x ε n & 1 ε n Join, 601, 2 628 x+1 ε n Detach, 626, 627 629 ALL(d):[x+1 ε n & d ε m => g(x+1,d) ε m] U Spec, 11 630 x+1 ε n & y ε m => g(x+1,y) ε m U Spec, 629 631 x+1 ε n & y ε m Join, 628, 605 632 g(x+1,y) ε m Detach, 630, 631 633 x+1 ε n & g(x+1,y) ε m Join, 628, 632 634 (x+1,g(x+1,y)) ε nm Detach, 624, 633 Suppose... 635 t ε s Premise 636 t ε s <=> t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] U Spec, 29 637 [t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]]] & [t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s] Iff-And, 636 638 t ε s => t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Split, 637 639 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] => t ε s Split, 637 640 t ε pnm & [(1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t]] Detach, 638, 635 641 t ε pnm Split, 640 642 (1,m1) ε t & ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 640 643 (1,m1) ε t Split, 642 644 ALL(b):ALL(c):[(b,c) ε t => (b+1,g(b+1,c)) ε t] Split, 642 645 ALL(c):[(x,c) ε t => (x+1,g(x+1,c)) ε t] U Spec, 644 646 (x,y) ε t => (x+1,g(x+1,y)) ε t U Spec, 645 647 t ε s => (x,y) ε t U Spec, 614 648 (x,y) ε t Detach, 647, 635 649 (x+1,g(x+1,y)) ε t Detach, 646, 648 650 ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Conclusion, 635 651 (x+1,g(x+1,y)) ε nm & ALL(c):[c ε s => (x+1,g(x+1,y)) ε c] Join, 634, 650 652 (x+1,g(x+1,y)) ε f Detach, 619, 651 653 ALL(d):[d=f(x) <=> (x,d) ε f] U Spec, 569 654 y=f(x) <=> (x,y) ε f U Spec, 653 655 [y=f(x) => (x,y) ε f] & [(x,y) ε f => y=f(x)] Iff-And, 654 656 y=f(x) => (x,y) ε f Split, 655 657 (x,y) ε f => y=f(x) Split, 655 658 y=f(x) Detach, 657, 606 659 ALL(d):[d=f(x+1) <=> (x+1,d) ε f] U Spec, 569 660 g(x+1,y)=f(x+1) <=> (x+1,g(x+1,y)) ε f U Spec, 659 661 [g(x+1,y)=f(x+1) => (x+1,g(x+1,y)) ε f] & [(x+1,g(x+1,y)) ε f => g(x+1,y)=f(x+1)] Iff-And, 660 662 g(x+1,y)=f(x+1) => (x+1,g(x+1,y)) ε f Split, 661 663 (x+1,g(x+1,y)) ε f => g(x+1,y)=f(x+1) Split, 661 664 g(x+1,y)=f(x+1) Detach, 663, 652 665 g(x+1,f(x))=f(x+1) Substitute, 658, 664 666 f(x+1)=g(x+1,f(x)) Sym, 665 667 ALL(c):[c ε n => f(c+1)=g(c+1,f(c))] Conclusion, 601 668 f(1)=m1 & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))] Join, 600, 667 As Required: 669 ALL(a):ALL(b):ALL(g):[Set(a) & b ε a & ALL(c):ALL(d):[c ε n & d ε a => g(c,d) ε a] => EXIST(f):[f(1)=b & ALL(c):[c ε n => f(c+1)=g(c+1,f(c))]]] Conclusion, 8