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