THEOREM

*******

 

From Peano's Axiom, we have:

 

EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]

& ALL(a):[a e n => add(a,0)=a]

& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]]

 

where

 

n    = the set of natural numbers

add  = the add function

next = the successor function on n

 

(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com)

 

 

Outline

*******

 

Construct:

 

1. n3, the set of ordered triples of n

2. pn3, the power set of n3

3. add, a subset of n3

 

Prove that n is a function with the required properties.

 

 

PEANO'S AXIOMS

**************

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

next is a function on n

 

3     ALL(a):[a e n => next(a) e n]

      Axiom

 

next is an injective (1-to-1) function

 

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

 

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

*****

 

Construct the set of ordered triples of n

 

Apply the Cartesian Product Axiom

 

7     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

 

8     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, 7

 

9     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, 8

 

10    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, 9

 

11    Set(n) & Set(n)

      Join, 1, 1

 

12    Set(n) & Set(n) & Set(n)

      Join, 11, 1

 

13    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, 10, 12

 

14    Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      E Spec, 13

 

 

Define: n3  (the set of ordered triples of n)

**********

 

15    Set''(n3)

      Split, 14

 

16    ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      Split, 14

 

 

Construct the powerset of n3

 

Apply the Power Set Axiom

 

17    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

 

18    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, 17

 

19    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, 18, 15

 

20    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, 19

 

 

Define: pn3  (the power set of n3)

***********

 

21    Set(pn3)

      Split, 20

 

22    ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]

      Split, 20

 

Construct the set add

 

Apply the Subset Axiom

 

23    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,e) e d]

     & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

     => (a,b,c) e d]]]

      Subset, 15

 

24    Set''(add) & ALL(a):ALL(b):ALL(c):[(a,b,c) e add

     <=> (a,b,c) e n3 & ALL(d):[d e pn3

     & ALL(e):[e e n => (e,0,e) e d]

     & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

     => (a,b,c) e d]]

      E Spec, 23

 

 

Define: add

***********

 

25    Set''(add)

      Split, 24

 

26    ALL(a):ALL(b):ALL(c):[(a,b,c) e add

     <=> (a,b,c) e n3 & ALL(d):[d e pn3

     & ALL(e):[e e n => (e,0,e) e d]

     & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

     => (a,b,c) e d]]

      Split, 24

 

    

     Derive some useful properties of add

     ************************************

    

     Prove: ALL(a):[a e n => (a,0,a) e add]

    

     Suppose...

 

      27    x e n

            Premise

 

      28    ALL(b):ALL(c):[(x,b,c) e add

          <=> (x,b,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,b,c) e d]]

            U Spec, 26

 

      29    ALL(c):[(x,0,c) e add

          <=> (x,0,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,c) e d]]

            U Spec, 28

 

      30    (x,0,x) e add

          <=> (x,0,x) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d]

            U Spec, 29

 

      31    [(x,0,x) e add => (x,0,x) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d]]

          & [(x,0,x) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d] => (x,0,x) e add]

            Iff-And, 30

 

      32    (x,0,x) e add => (x,0,x) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d]

            Split, 31

 

     Sufficient: (x,0,x) e add

 

      33    (x,0,x) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d] => (x,0,x) e add

            Split, 31

 

      34    ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 16

 

      35    ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]

            U Spec, 34

 

      36    (x,0,x) e n3 <=> x e n & 0 e n & x e n

            U Spec, 35

 

      37    [(x,0,x) e n3 => x e n & 0 e n & x e n]

          & [x e n & 0 e n & x e n => (x,0,x) e n3]

            Iff-And, 36

 

      38    (x,0,x) e n3 => x e n & 0 e n & x e n

            Split, 37

 

      39    x e n & 0 e n & x e n => (x,0,x) e n3

            Split, 37

 

      40    x e n & 0 e n

            Join, 27, 2

 

      41    x e n & 0 e n & x e n

            Join, 40, 27

 

      42    (x,0,x) e n3

            Detach, 39, 41

 

         

          Prove: ALL(d):[d e pn3

                 & ALL(e):[e e n => (e,0,e) e d]

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                 => (x,0,x) e d]

         

          Suppose...

 

            43    q e pn3

              & ALL(e):[e e n => (e,0,e) e q]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                  Premise

 

            44    q e pn3

                  Split, 43

 

            45    ALL(e):[e e n => (e,0,e) e q]

                  Split, 43

 

            46    ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                  Split, 43

 

            47    x e n => (x,0,x) e q

                  U Spec, 45

 

            48    (x,0,x) e q

                  Detach, 47, 27

 

     As Required:

 

      49    ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d]

            4 Conclusion, 43

 

      50    (x,0,x) e n3

          & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,0,x) e d]

            Join, 42, 49

 

      51    (x,0,x) e add

            Detach, 33, 50

 

As Required:

 

52    ALL(a):[a e n => (a,0,a) e add]

      4 Conclusion, 27

 

    

     Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

            => [(a,b,c) e add => (a,next(b),next(c)) e add]]

    

     Suppose...

 

      53    x e n & y e n & z e n

            Premise

 

      54    x e n

            Split, 53

 

      55    y e n

            Split, 53

 

      56    z e n

            Split, 53

 

         

          Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

                 => [(a,b,c) e add => (a,next(b),next(c)) e add]]

         

          Suppose...

 

            57    (x,y,z) e add

                  Premise

 

            58    ALL(b):ALL(c):[(x,b,c) e add

              <=> (x,b,c) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,b,c) e d]]

                  U Spec, 26

 

            59    ALL(c):[(x,y,c) e add

              <=> (x,y,c) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,c) e d]]

                  U Spec, 58

 

            60    (x,y,z) e add

              <=> (x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d]

                  U Spec, 59

 

            61    [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d]]

              & [(x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d] => (x,y,z) e add]

                  Iff-And, 60

 

            62    (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d]

                  Split, 61

 

            63    (x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d] => (x,y,z) e add

                  Split, 61

 

            64    (x,y,z) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d]

                  Detach, 62, 57

 

            65    (x,y,z) e n3

                  Split, 64

 

            66    ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,y,z) e d]

                  Split, 64

 

            67    ALL(b):ALL(c):[(x,b,c) e add

              <=> (x,b,c) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,b,c) e d]]

                  U Spec, 26

 

            68    ALL(c):[(x,next(y),c) e add

              <=> (x,next(y),c) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),c) e d]]

                  U Spec, 67

 

            69    (x,next(y),next(z)) e add

              <=> (x,next(y),next(z)) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d]

                  U Spec, 68

 

            70    [(x,next(y),next(z)) e add => (x,next(y),next(z)) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d]]

              & [(x,next(y),next(z)) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d] => (x,next(y),next(z)) e add]

                  Iff-And, 69

 

            71    (x,next(y),next(z)) e add => (x,next(y),next(z)) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d]

                  Split, 70

 

          Sufficient: (x,next(y),next(z)) e add

 

            72    (x,next(y),next(z)) e n3 & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d] => (x,next(y),next(z)) e add

                  Split, 70

 

            73    ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 16

 

            74    ALL(c3):[(x,next(y),c3) e n3 <=> x e n & next(y) e n & c3 e n]

                  U Spec, 73

 

            75    (x,next(y),next(z)) e n3 <=> x e n & next(y) e n & next(z) e n

                  U Spec, 74

 

            76    [(x,next(y),next(z)) e n3 => x e n & next(y) e n & next(z) e n]

              & [x e n & next(y) e n & next(z) e n => (x,next(y),next(z)) e n3]

                  Iff-And, 75

 

            77    (x,next(y),next(z)) e n3 => x e n & next(y) e n & next(z) e n

                  Split, 76

 

            78    x e n & next(y) e n & next(z) e n => (x,next(y),next(z)) e n3

                  Split, 76

 

            79    y e n => next(y) e n

                  U Spec, 3

 

            80    next(y) e n

                  Detach, 79, 55

 

            81    z e n => next(z) e n

                  U Spec, 3

 

            82    next(z) e n

                  Detach, 81, 56

 

            83    x e n & next(y) e n

                  Join, 54, 80

 

            84    x e n & next(y) e n & next(z) e n

                  Join, 83, 82

 

            85    (x,next(y),next(z)) e n3

                  Detach, 78, 84

 

             

              Prove: ALL(d):[d e pn3

                     & ALL(e):[e e n => (e,0,e) e d]

                     & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                     => (x,next(y),next(z)) e d]

             

              Suppose...

 

                  86    q e pn3

                   & ALL(e):[e e n => (e,0,e) e q]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                        Premise

 

                  87    q e pn3

                        Split, 86

 

                  88    ALL(e):[e e n => (e,0,e) e q]

                        Split, 86

 

                  89    ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                        Split, 86

 

                  90    ALL(f):ALL(g):[(x,f,g) e q => (x,next(f),next(g)) e q]

                        U Spec, 89

 

                  91    ALL(g):[(x,y,g) e q => (x,next(y),next(g)) e q]

                        U Spec, 90

 

              Sufficient: (x,next(y),next(z)) e q

 

                  92    (x,y,z) e q => (x,next(y),next(z)) e q

                        U Spec, 91

 

              Sufficient: (x,y,z) e q

 

                  93    q e pn3

                   & ALL(e):[e e n => (e,0,e) e q]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                   => (x,y,z) e q

                        U Spec, 66

 

                  94    (x,y,z) e q

                        Detach, 93, 86

 

                  95    (x,next(y),next(z)) e q

                        Detach, 92, 94

 

          As Required:

 

            96    ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d]

                  4 Conclusion, 86

 

            97    (x,next(y),next(z)) e n3

              & ALL(d):[d e pn3

              & ALL(e):[e e n => (e,0,e) e d]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

              => (x,next(y),next(z)) e d]

                  Join, 85, 96

 

            98    (x,next(y),next(z)) e add

                  Detach, 72, 97

 

     As Required:

 

      99    (x,y,z) e add => (x,next(y),next(z)) e add

            4 Conclusion, 57

 

As Required:

 

100  ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

     => [(a,b,c) e add => (a,next(b),next(c)) e add]]

      4 Conclusion, 53

 

    

     Prove: ALL(a):[aen => ALL(b):[ben => [(a,0,b)eadd  => b=a]]]

    

     Suppose...

 

      101  x e n

            Premise

 

         

          Prove: ALL(b):[b e n => [(x,0,b) e add => b=x]]

         

          Suppose...

 

            102  z e n

                  Premise

 

             

              Prove: (x,0,z) e add & ~z=x

             

              Suppose to the contrary...

 

                  103  (x,0,z) e add & ~z=x

                        Premise

 

                  104  (x,0,z) e add

                        Split, 103

 

                  105  ~z=x

                        Split, 103

 

                  106  ALL(b):ALL(c):[(x,b,c) e add

                   <=> (x,b,c) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,b,c) e d]]

                        U Spec, 26

 

                  107  ALL(c):[(x,0,c) e add

                   <=> (x,0,c) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,c) e d]]

                        U Spec, 106

 

                  108  (x,0,z) e add

                   <=> (x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d]

                        U Spec, 107

 

                  109  [(x,0,z) e add => (x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d]]

                   & [(x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d] => (x,0,z) e add]

                        Iff-And, 108

 

                  110  (x,0,z) e add => (x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d]

                        Split, 109

 

                  111  (x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d] => (x,0,z) e add

                        Split, 109

 

                  112  ~[(x,0,z) e n3 & ALL(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   => (x,0,z) e d]] => ~(x,0,z) e add

                        Contra, 110

 

                  113  ~[(x,0,z) e n3 & ALL(d):~[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d]] => ~(x,0,z) e add

                        Imply-And, 112

 

                  114  ~~[~(x,0,z) e n3 | ~ALL(d):~[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d]] => ~(x,0,z) e add

                        DeMorgan, 113

 

                  115  ~(x,0,z) e n3 | ~ALL(d):~[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add

                        Rem DNeg, 114

 

                  116  ~(x,0,z) e n3 | ~~EXIST(d):~~[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add

                        Quant, 115

 

                  117  ~(x,0,z) e n3 | EXIST(d):~~[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add

                        Rem DNeg, 116

 

              Sufficient: ~(x,0,z) e add   (to obtain a contradiction)

             

              Use d=q as defined below

 

                  118  ~(x,0,z) e n3 | EXIST(d):[d e pn3

                   & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add

                        Rem DNeg, 117

 

                  119  EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

                   <=> (a,b,c) e add & ~[a=x & b=0 & c=z]]]

                        Subset, 25

 

                  120  Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                   <=> (a,b,c) e add & ~[a=x & b=0 & c=z]]

                        E Spec, 119

 

              Define: q

              *********

 

                  121  Set''(q)

                        Split, 120

 

                  122  ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                   <=> (a,b,c) e add & ~[a=x & b=0 & c=z]]

                        Split, 120

 

                  123  q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        U Spec, 22

 

                  124  [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]

                   & [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]

                        Iff-And, 123

 

                  125  q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        Split, 124

 

              Sufficient: q e pn3

 

                  126  Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3

                        Split, 124

 

                  

                   Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                  

                   Suppose...

 

                        127  (t,u,v) e q

                              Premise

 

                        128  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e add & ~[t=x & b=0 & c=z]]

                              U Spec, 122

 

                        129  ALL(c):[(t,u,c) e q

                        <=> (t,u,c) e add & ~[t=x & u=0 & c=z]]

                              U Spec, 128

 

                        130  (t,u,v) e q

                        <=> (t,u,v) e add & ~[t=x & u=0 & v=z]

                              U Spec, 129

 

                        131  [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]]

                        & [(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q]

                              Iff-And, 130

 

                        132  (t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]

                              Split, 131

 

                        133  (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q

                              Split, 131

 

                        134  (t,u,v) e add & ~[t=x & u=0 & v=z]

                              Detach, 132, 127

 

                        135  (t,u,v) e add

                              Split, 134

 

                        136  ~[t=x & u=0 & v=z]

                              Split, 134

 

                        137  ALL(b):ALL(c):[(t,b,c) e add

                        <=> (t,b,c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,b,c) e d]]

                              U Spec, 26

 

                        138  ALL(c):[(t,u,c) e add

                        <=> (t,u,c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,c) e d]]

                              U Spec, 137

 

                        139  (t,u,v) e add

                        <=> (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              U Spec, 138

 

                        140  [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]]

                        & [(t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d] => (t,u,v) e add]

                              Iff-And, 139

 

                        141  (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              Split, 140

 

                        142  (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d] => (t,u,v) e add

                              Split, 140

 

                        143  (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              Detach, 141, 135

 

                        144  (t,u,v) e n3

                              Split, 143

 

                  145  ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        4 Conclusion, 127

 

                  146  Set''(q)

                   & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        Join, 121, 145

 

              As Required:

 

                  147  q e pn3

                        Detach, 126, 146

 

                  

                   Prove: ALL(e):[e e n => (e,0,e) e q]

                  

                   Suppose...

 

                        148  t e n

                              Premise

 

                        149  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e add & ~[t=x & b=0 & c=z]]

                              U Spec, 122

 

                        150  ALL(c):[(t,0,c) e q

                        <=> (t,0,c) e add & ~[t=x & 0=0 & c=z]]

                              U Spec, 149

 

                        151  (t,0,t) e q

                        <=> (t,0,t) e add & ~[t=x & 0=0 & t=z]

                              U Spec, 150

 

                        152  [(t,0,t) e q => (t,0,t) e add & ~[t=x & 0=0 & t=z]]

                        & [(t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q]

                              Iff-And, 151

 

                        153  (t,0,t) e q => (t,0,t) e add & ~[t=x & 0=0 & t=z]

                              Split, 152

 

                   Sufficient: (t,0,t) e q

 

                        154  (t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q

                              Split, 152

 

                        155  t e n => (t,0,t) e add

                              U Spec, 52

 

                        156  (t,0,t) e add

                              Detach, 155, 148

 

                       

                        Prove: ~[t=x & 0=0 & t=z]

                       

                        Suppose to the contrary...

 

                              157  t=x & 0=0 & t=z

                                    Premise

 

                              158  t=x

                                    Split, 157

 

                              159  0=0

                                    Split, 157

 

                              160  t=z

                                    Split, 157

 

                              161  z=x

                                    Substitute, 160, 158

 

                        Obtain the contradiction...

 

                              162  z=x & ~z=x

                                    Join, 161, 105

 

                   As Required:

 

                        163  ~[t=x & 0=0 & t=z]

                              4 Conclusion, 157

 

                        164  (t,0,t) e add & ~[t=x & 0=0 & t=z]

                              Join, 156, 163

 

                        165  (t,0,t) e q

                              Detach, 154, 164

 

              As Required:

 

                  166  ALL(e):[e e n => (e,0,e) e q]

                        4 Conclusion, 148

 

                  

                   Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                  

                   Suppose...

 

                        167  (t,u,v) e q

                              Premise

 

                        168  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e add & ~[t=x & b=0 & c=z]]

                              U Spec, 122

 

                        169  ALL(c):[(t,u,c) e q

                        <=> (t,u,c) e add & ~[t=x & u=0 & c=z]]

                              U Spec, 168

 

                        170  (t,u,v) e q

                        <=> (t,u,v) e add & ~[t=x & u=0 & v=z]

                              U Spec, 169

 

                        171  [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]]

                        & [(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q]

                              Iff-And, 170

 

                        172  (t,u,v) e q => (t,u,v) e add & ~[t=x & u=0 & v=z]

                              Split, 171

 

                        173  (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q

                              Split, 171

 

                        174  (t,u,v) e add & ~[t=x & u=0 & v=z]

                              Detach, 172, 167

 

                        175  (t,u,v) e add

                              Split, 174

 

                        176  ~[t=x & u=0 & v=z]

                              Split, 174

 

                        177  ALL(b):ALL(c):[(t,b,c) e add

                        <=> (t,b,c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,b,c) e d]]

                              U Spec, 26

 

                        178  ALL(c):[(t,u,c) e add

                        <=> (t,u,c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,c) e d]]

                              U Spec, 177

 

                        179  (t,u,v) e add

                        <=> (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              U Spec, 178

 

                        180  [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]]

                        & [(t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d] => (t,u,v) e add]

                              Iff-And, 179

 

                        181  (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              Split, 180

 

                        182  (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d] => (t,u,v) e add

                              Split, 180

 

                        183  (t,u,v) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              Detach, 181, 175

 

                        184  (t,u,v) e n3

                              Split, 183

 

                        185  ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (t,u,v) e d]

                              Split, 183

 

                        186  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e add & ~[t=x & b=0 & c=z]]

                              U Spec, 122

 

                        187  ALL(c):[(t,next(u),c) e q

                        <=> (t,next(u),c) e add & ~[t=x & next(u)=0 & c=z]]

                              U Spec, 186

 

                        188  (t,next(u),next(v)) e q

                        <=> (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]

                              U Spec, 187

 

                        189  [(t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]]

                        & [(t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z] => (t,next(u),next(v)) e q]

                              Iff-And, 188

 

                        190  (t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z]

                              Split, 189

 

                   Sufficient: (t,next(u),next(v)) e q

 

                        191  (t,next(u),next(v)) e add & ~[t=x & next(u)=0 & next(v)=z] => (t,next(u),next(v)) e q

                              Split, 189

 

                        192  ALL(b):ALL(c):[t e n & b e n & c e n

                        => [(t,b,c) e add => (t,next(b),next(c)) e add]]

                              U Spec, 100

 

                        193  ALL(c):[t e n & u e n & c e n

                        => [(t,u,c) e add => (t,next(u),next(c)) e add]]

                              U Spec, 192

 

                        194  t e n & u e n & v e n

                        => [(t,u,v) e add => (t,next(u),next(v)) e add]

                              U Spec, 193

 

                        195  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                              U Spec, 16

 

                        196  ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]

                              U Spec, 195

 

                        197  (t,u,v) e n3 <=> t e n & u e n & v e n

                              U Spec, 196

 

                        198  [(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, 197

 

                        199  (t,u,v) e n3 => t e n & u e n & v e n

                              Split, 198

 

                        200  t e n & u e n & v e n => (t,u,v) e n3

                              Split, 198

 

                        201  t e n & u e n & v e n

                              Detach, 199, 184

 

                        202  t e n

                              Split, 201

 

                        203  u e n

                              Split, 201

 

                        204  v e n

                              Split, 201

 

                        205  (t,u,v) e add => (t,next(u),next(v)) e add

                              Detach, 194, 201

 

                   As Required:

 

                        206  (t,next(u),next(v)) e add

                              Detach, 205, 175

 

                       

                        Prove: ~[t=x & next(u)=0 & next(v)=z]

                       

                        Suppose to the contrary...

 

                              207  t=x & next(u)=0 & next(v)=z

                                    Premise

 

                              208  t=x

                                    Split, 207

 

                              209  next(u)=0

                                    Split, 207

 

                              210  next(v)=z

                                    Split, 207

 

                              211  u e n => ~next(u)=0

                                    U Spec, 5

 

                              212  ~next(u)=0

                                    Detach, 211, 203

 

                        Obtain the contradiction...

 

                              213  next(u)=0 & ~next(u)=0

                                    Join, 209, 212

 

                   As Required:

 

                        214  ~[t=x & next(u)=0 & next(v)=z]

                              4 Conclusion, 207

 

                        215  (t,next(u),next(v)) e add

                        & ~[t=x & next(u)=0 & next(v)=z]

                              Join, 206, 214

 

                        216  (t,next(u),next(v)) e q

                              Detach, 191, 215

 

              As Required:

 

                  217  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                        4 Conclusion, 167

 

                  218  ALL(b):ALL(c):[(x,b,c) e q

                   <=> (x,b,c) e add & ~[x=x & b=0 & c=z]]

                        U Spec, 122

 

                  219  ALL(c):[(x,0,c) e q

                   <=> (x,0,c) e add & ~[x=x & 0=0 & c=z]]

                        U Spec, 218

 

                  220  (x,0,z) e q

                   <=> (x,0,z) e add & ~[x=x & 0=0 & z=z]

                        U Spec, 219

 

                  221  [(x,0,z) e q => (x,0,z) e add & ~[x=x & 0=0 & z=z]]

                   & [(x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q]

                        Iff-And, 220

 

                  222  (x,0,z) e q => (x,0,z) e add & ~[x=x & 0=0 & z=z]

                        Split, 221

 

                  223  (x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q

                        Split, 221

 

                  224  ~[(x,0,z) e add & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q

                        Contra, 222

 

                  225  ~~[~(x,0,z) e add | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q

                        DeMorgan, 224

 

                  226  ~(x,0,z) e add | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q

                        Rem DNeg, 225

 

                  227  ~(x,0,z) e add | x=x & 0=0 & z=z => ~(x,0,z) e q

                        Rem DNeg, 226

 

                  228  x=x

                        Reflex

 

                  229  0=0

                        Reflex

 

                  230  z=z

                        Reflex

 

                  231  x=x & 0=0

                        Join, 228, 229

 

                  232  x=x & 0=0 & z=z

                        Join, 231, 230

 

                  233  ~(x,0,z) e add | x=x & 0=0 & z=z

                        Arb Or, 232

 

              As Required:

 

                  234  ~(x,0,z) e q

                        Detach, 227, 233

 

                  235  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                        Join, 147, 166

 

                  236  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                        Join, 235, 217

 

                  237  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                   & ~(x,0,z) e q

                        Join, 236, 234

 

                  238  EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   & ~(x,0,z) e d]

                        E Gen, 237

 

                  239  ~(x,0,z) e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                   & ~(x,0,z) e d]

                        Arb Or, 238

 

                  240  ~(x,0,z) e add

                        Detach, 118, 239

 

                  241  (x,0,z) e add & ~(x,0,z) e add

                        Join, 104, 240

 

          As Required:

 

            242  ~[(x,0,z) e add & ~z=x]

                  4 Conclusion, 103

 

            243  ~~[(x,0,z) e add => ~~z=x]

                  Imply-And, 242

 

            244  (x,0,z) e add => ~~z=x

                  Rem DNeg, 243

 

            245  (x,0,z) e add => z=x

                  Rem DNeg, 244

 

     As Required:

 

      246  ALL(b):[b e n => [(x,0,b) e add => b=x]]

            4 Conclusion, 102

 

As Required:

 

247  ALL(a):[a e n => ALL(b):[b e n => [(a,0,b) e add => b=a]]]

      4 Conclusion, 101

 

248  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

 

249  ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => 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 add]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]

      U Spec, 248

 

250  ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => 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 add]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]

      U Spec, 249

 

251  ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => 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 add]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]

      U Spec, 250

 

Sufficient: For functionality of add

 

252  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => 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 add]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]

      U Spec, 251

 

    

     Prove: ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]

    

     Suppose...

 

      253  (x,y,z) e add

            Premise

 

      254  ALL(b):ALL(c):[(x,b,c) e add

          <=> (x,b,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,b,c) e d]]

            U Spec, 26

 

      255  ALL(c):[(x,y,c) e add

          <=> (x,y,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,c) e d]]

            U Spec, 254

 

      256  (x,y,z) e add

          <=> (x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d]

            U Spec, 255

 

      257  [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d]]

          & [(x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d] => (x,y,z) e add]

            Iff-And, 256

 

      258  (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d]

            Split, 257

 

      259  (x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d] => (x,y,z) e add

            Split, 257

 

      260  (x,y,z) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d]

            Detach, 258, 253

 

      261  (x,y,z) e n3

            Split, 260

 

      262  ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z) e d]

            Split, 260

 

      263  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 16

 

      264  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

            U Spec, 263

 

      265  (x,y,z) e n3 <=> x e n & y e n & z e n

            U Spec, 264

 

      266  [(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, 265

 

      267  (x,y,z) e n3 => x e n & y e n & z e n

            Split, 266

 

      268  x e n & y e n & z e n => (x,y,z) e n3

            Split, 266

 

      269  x e n & y e n & z e n

            Detach, 267, 261

 

As Required: Functionality, Part 1

 

270  ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]

      4 Conclusion, 253

 

    

     Prove: ALL(a):[a e n => EXIST(b):[b e n & (a,0,b) e add]]

    

     Suppose...

 

      271  x e n

            Premise

 

      272  x e n => (x,0,x) e add

            U Spec, 52

 

      273  (x,0,x) e add

            Detach, 272, 271

 

      274  x e n & (x,0,x) e add

            Join, 271, 273

 

      275  EXIST(b):[b e n & (x,0,b) e add]

            E Gen, 274

 

As Required:

 

276  ALL(a):[a e n => EXIST(b):[b e n & (a,0,b) e add]]

      4 Conclusion, 271

 

    

     Prove: ALL(a):[a e n

            => ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e add]]]

    

     Suppose...

 

      277  x e n

            Premise

 

      278  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]]

            Subset, 1

 

      279  Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]

            E Spec, 278

 

    

     Prove: p1

     *********

 

      280  Set(p1)

            Split, 279

 

      281  ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]

            Split, 279

 

     Apply PMI axiom

 

      282  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...

 

            283  y e p1

                  Premise

 

            284  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]

                  U Spec, 281

 

            285  [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]

              & [y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]

                  Iff-And, 284

 

            286  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Split, 285

 

            287  y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1

                  Split, 285

 

            288  y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Detach, 286, 283

 

            289  y e n

                  Split, 288

 

     As Required:

 

      290  ALL(b):[b e p1 => b e n]

            4 Conclusion, 283

 

      291  Set(p1) & ALL(b):[b e p1 => b e n]

            Join, 280, 290

 

    

     Sufficient: ALL(b):[b e n => b e p1]

 

      292  0 e p1 & ALL(b):[b e p1 => next(b) e p1]

          => ALL(b):[b e n => b e p1]

            Detach, 282, 291

 

      293  0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e add]

            U Spec, 281

 

      294  [0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e add]]

          & [0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1]

            Iff-And, 293

 

      295  0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e add]

            Split, 294

 

     Sufficient: 0 e p1

 

      296  0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1

            Split, 294

 

      297  x e n => EXIST(b):[b e n & (x,0,b) e add]

            U Spec, 276

 

      298  EXIST(b):[b e n & (x,0,b) e add]

            Detach, 297, 277

 

      299  0 e n & EXIST(b):[b e n & (x,0,b) e add]

            Join, 2, 298

 

     As Required:

 

      300  0 e p1

            Detach, 296, 299

 

         

          Prove: ALL(b):[b e p1 => next(b) e p1]

         

          Suppose...

 

            301  y e p1

                  Premise

 

            302  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]

                  U Spec, 281

 

            303  [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]

              & [y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]

                  Iff-And, 302

 

            304  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Split, 303

 

            305  y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1

                  Split, 303

 

            306  y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Detach, 304, 301

 

            307  y e n

                  Split, 306

 

            308  EXIST(c):[c e n & (x,y,c) e add]

                  Split, 306

 

            309  z e n & (x,y,z) e add

                  E Spec, 308

 

            310  z e n

                  Split, 309

 

            311  (x,y,z) e add

                  Split, 309

 

            312  next(y) e p1 <=> next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]

                  U Spec, 281

 

            313  [next(y) e p1 => next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]]

              & [next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add] => next(y) e p1]

                  Iff-And, 312

 

            314  next(y) e p1 => next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add]

                  Split, 313

 

          Sufficient: next(y) e p1

 

            315  next(y) e n & EXIST(c):[c e n & (x,next(y),c) e add] => next(y) e p1

                  Split, 313

 

            316  y e n => next(y) e n

                  U Spec, 3

 

            317  next(y) e n

                  Detach, 316, 307

 

            318  ALL(b):ALL(c):[x e n & b e n & c e n

              => [(x,b,c) e add => (x,next(b),next(c)) e add]]

                  U Spec, 100

 

            319  ALL(c):[x e n & y e n & c e n

              => [(x,y,c) e add => (x,next(y),next(c)) e add]]

                  U Spec, 318

 

            320  x e n & y e n & z e n

              => [(x,y,z) e add => (x,next(y),next(z)) e add]

                  U Spec, 319

 

            321  x e n & y e n

                  Join, 277, 307

 

            322  x e n & y e n & z e n

                  Join, 321, 310

 

            323  (x,y,z) e add => (x,next(y),next(z)) e add

                  Detach, 320, 322

 

            324  (x,next(y),next(z)) e add

                  Detach, 323, 311

 

            325  z e n => next(z) e n

                  U Spec, 3

 

            326  next(z) e n

                  Detach, 325, 310

 

            327  next(z) e n & (x,next(y),next(z)) e add

                  Join, 326, 324

 

            328  EXIST(c):[c e n & (x,next(y),c) e add]

                  E Gen, 327

 

            329  next(y) e n

              & EXIST(c):[c e n & (x,next(y),c) e add]

                  Join, 317, 328

 

            330  next(y) e p1

                  Detach, 315, 329

 

     As Required:

 

      331  ALL(b):[b e p1 => next(b) e p1]

            4 Conclusion, 301

 

      332  0 e p1 & ALL(b):[b e p1 => next(b) e p1]

            Join, 300, 331

 

     As Required:

 

      333  ALL(b):[b e n => b e p1]

            Detach, 292, 332

 

         

          Prove: ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]

         

          Suppose...

 

            334  y e n

                  Premise

 

            335  y e n => y e p1

                  U Spec, 333

 

            336  y e p1

                  Detach, 335, 334

 

            337  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]

                  U Spec, 281

 

            338  [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]

              & [y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]

                  Iff-And, 337

 

            339  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Split, 338

 

            340  y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1

                  Split, 338

 

            341  y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Detach, 339, 336

 

            342  y e n & EXIST(c):[c e n & (x,y,c) e add]

                  Detach, 339, 336

 

            343  y e n

                  Split, 342

 

            344  EXIST(c):[c e n & (x,y,c) e add]

                  Split, 342

 

     As Required:

 

      345  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]

            4 Conclusion, 334

 

As Required:

 

346  ALL(a):[a e n

     => ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e add]]]

      4 Conclusion, 277

 

    

     Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]

    

     Suppose...

 

      347  x e n & y e n

            Premise

 

      348  x e n

            Split, 347

 

      349  y e n

            Split, 347

 

      350  x e n

          => ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]

            U Spec, 346

 

      351  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e add]]

            Detach, 350, 348

 

      352  y e n => EXIST(c):[c e n & (x,y,c) e add]

            U Spec, 351

 

      353  EXIST(c):[c e n & (x,y,c) e add]

            Detach, 352, 349

 

As Required: Functionality, Part 2

 

354  ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]

      4 Conclusion, 347

 

    

     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 add & (a,b,c2) e add => c1=c2]]]]

    

     Suppose...

 

      355  x e n

            Premise

 

      356  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 add & (x,b,c2) e add => c1=c2]]]]

            Subset, 1

 

      357  Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

            E Spec, 356

 

    

     Define: p2

     **********

 

      358  Set(p2)

            Split, 357

 

      359  ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

            Split, 357

 

      360  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...

 

            361  y e p2

                  Premise

 

            362  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  U Spec, 359

 

            363  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]

              & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]

                  Iff-And, 362

 

            364  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Split, 363

 

            365  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2

                  Split, 363

 

            366  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Detach, 364, 361

 

            367  y e n

                  Split, 366

 

     As Required:

 

      368  ALL(b):[b e p2 => b e n]

            4 Conclusion, 361

 

      369  Set(p2) & ALL(b):[b e p2 => b e n]

            Join, 358, 368

 

     Sufficient: ALL(b):[b e n => b e p2]

 

      370  0 e p2 & ALL(b):[b e p2 => next(b) e p2]

          => ALL(b):[b e n => b e p2]

            Detach, 360, 369

 

      371  0 e p2 <=> 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]

            U Spec, 359

 

      372  [0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]]

          & [0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]] => 0 e p2]

            Iff-And, 371

 

      373  0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]

            Split, 372

 

     Sufficient: 0 e p2

 

      374  0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]] => 0 e p2

            Split, 372

 

         

          Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n

                 => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]

         

          Suppose...

 

            375  z1 e n & z2 e n

                  Premise

 

            376  z1 e n

                  Split, 375

 

            377  z2 e n

                  Split, 375

 

             

              Prove: (x,0,z1) e add & (x,0,z2) e add => z1=z2

             

              Suppose...

 

                  378  (x,0,z1) e add & (x,0,z2) e add

                        Premise

 

                  379  (x,0,z1) e add

                        Split, 378

 

                  380  (x,0,z2) e add

                        Split, 378

 

                  381  x e n => ALL(b):[b e n => [(x,0,b) e add => b=x]]

                        U Spec, 247

 

                  382  ALL(b):[b e n => [(x,0,b) e add => b=x]]

                        Detach, 381, 355

 

                  383  z1 e n => [(x,0,z1) e add => z1=x]

                        U Spec, 382

 

                  384  (x,0,z1) e add => z1=x

                        Detach, 383, 376

 

                  385  z1=x

                        Detach, 384, 379

 

                  386  z2 e n => [(x,0,z2) e add => z2=x]

                        U Spec, 382

 

                  387  (x,0,z2) e add => z2=x

                        Detach, 386, 377

 

                  388  z2=x

                        Detach, 387, 380

 

                  389  z1=z2

                        Substitute, 388, 385

 

          As Required:

 

            390  (x,0,z1) e add & (x,0,z2) e add => z1=z2

                  4 Conclusion, 378

 

     As Required:

 

      391  ALL(c1):ALL(c2):[c1 e n & c2 e n

          => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]

            4 Conclusion, 375

 

      392  0 e n

          & ALL(c1):ALL(c2):[c1 e n & c2 e n

          => [(x,0,c1) e add & (x,0,c2) e add => c1=c2]]

            Join, 2, 391

 

     As Required:

 

      393  0 e p2

            Detach, 374, 392

 

         

          Prove: ALL(b):[b e p2 => next(b) e p2]

         

          Suppose...

 

            394  y e p2

                  Premise

 

            395  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  U Spec, 359

 

            396  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]

              & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]

                  Iff-And, 395

 

            397  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Split, 396

 

            398  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2

                  Split, 396

 

            399  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Detach, 397, 394

 

            400  y e n

                  Split, 399

 

            401  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Split, 399

 

            402  next(y) e p2 <=> next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]

                  U Spec, 359

 

            403  [next(y) e p2 => next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]]

              & [next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]] => next(y) e p2]

                  Iff-And, 402

 

            404  next(y) e p2 => next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]

                  Split, 403

 

          Sufficient: next(y) e p2

 

            405  next(y) e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]] => next(y) e p2

                  Split, 403

 

            406  y e n => next(y) e n

                  U Spec, 3

 

            407  next(y) e n

                  Detach, 406, 400

 

            408  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e add]]

                  U Spec, 354

 

            409  x e n & y e n => EXIST(c):[c e n & (x,y,c) e add]

                  U Spec, 408

 

            410  x e n & y e n

                  Join, 355, 400

 

            411  EXIST(c):[c e n & (x,y,c) e add]

                  Detach, 409, 410

 

            412  z e n & (x,y,z) e add

                  E Spec, 411

 

          Define: z

 

            413  z e n

                  Split, 412

 

            414  (x,y,z) e add

                  Split, 412

 

             

              Prove: ALL(c):[c e n => [(x,y,c) e add => z=c]]

             

              Suppose...

 

                  415  z' e n

                        Premise

 

                  416  ALL(c2):[z e n & c2 e n => [(x,y,z) e add & (x,y,c2) e add => z=c2]]

                        U Spec, 401

 

                  417  z e n & z' e n => [(x,y,z) e add & (x,y,z') e add => z=z']

                        U Spec, 416

 

                  418  z e n & z' e n

                        Join, 413, 415

 

                  419  (x,y,z) e add & (x,y,z') e add => z=z'

                        Detach, 417, 418

 

                  

                   Prove: (x,y,z') e add => z=z'

                  

                   Suppose...

 

                        420  (x,y,z') e add

                              Premise

 

                        421  (x,y,z) e add & (x,y,z') e add

                              Join, 414, 420

 

                        422  z=z'

                              Detach, 419, 421

 

              As Required:

 

                  423  (x,y,z') e add => z=z'

                        4 Conclusion, 420

 

          As Required:

 

            424  ALL(c):[c e n => [(x,y,c) e add => z=c]]

                  4 Conclusion, 415

 

             

              Prove: ALL(c'):[c' e n => [(x,next(y),c') e add => c'=next(z)]]

             

              Suppose...

 

                  425  z' e n

                        Premise

 

                  

                   Prove: (x,next(y),z') e add & ~z'=next(z)

                  

                   Suppose to the contrary...

 

                        426  (x,next(y),z') e add & ~z'=next(z)

                              Premise

 

                        427  (x,next(y),z') e add

                              Split, 426

 

                        428  ~z'=next(z)

                              Split, 426

 

                        429  ALL(b):ALL(c):[(x,b,c) e add

                        <=> (x,b,c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,b,c) e d]]

                              U Spec, 26

 

                        430  ALL(c):[(x,next(y),c) e add

                        <=> (x,next(y),c) e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),c) e d]]

                              U Spec, 429

 

                        431  (x,next(y),z') e add

                        <=> (x,next(y),z') e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d]

                              U Spec, 430

 

                        432  [(x,next(y),z') e add => (x,next(y),z') e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) 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,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d] => (x,next(y),z') e add]

                              Iff-And, 431

 

                        433  (x,next(y),z') e add => (x,next(y),z') e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d]

                              Split, 432

 

                        434  (x,next(y),z') e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d] => (x,next(y),z') e add

                              Split, 432

 

                        435  ~[(x,next(y),z') e n3 & ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d]] => ~(x,next(y),z') e add

                              Contra, 433

 

                        436  ~~[~(x,next(y),z') e n3 | ~ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d]] => ~(x,next(y),z') e add

                              DeMorgan, 435

 

                        437  ~(x,next(y),z') e n3 | ~ALL(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d] => ~(x,next(y),z') e add

                              Rem DNeg, 436

 

                        438  ~(x,next(y),z') e n3 | ~~EXIST(d):~[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d] => ~(x,next(y),z') e add

                              Quant, 437

 

                        439  ~(x,next(y),z') e n3 | EXIST(d):~[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        => (x,next(y),z') e d] => ~(x,next(y),z') e add

                              Rem DNeg, 438

 

                        440  ~(x,next(y),z') e n3 | EXIST(d):~~[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,next(y),z') e d] => ~(x,next(y),z') e add

                              Imply-And, 439

 

                   Sufficient: ~(x,next(y),z') e add   (to obtain contradiction)

                  

                   Use d=q as defined below

 

                        441  ~(x,next(y),z') e n3 | EXIST(d):[d e pn3

                        & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d] & ~(x,next(y),z') e d] => ~(x,next(y),z') e add

                              Rem DNeg, 440

 

                        442  EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

                        <=> (a,b,c) e add & ~[a=x & b=next(y) & c=z']]]

                              Subset, 25

 

                        443  Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                        <=> (a,b,c) e add & ~[a=x & b=next(y) & c=z']]

                              E Spec, 442

 

                    Define: q

 

                        444  Set''(q)

                              Split, 443

 

                        445  ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                        <=> (a,b,c) e add & ~[a=x & b=next(y) & c=z']]

                              Split, 443

 

                        446  q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                              U Spec, 22

 

                        447  [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]

                        & [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]

                              Iff-And, 446

 

                        448  q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                              Split, 447

 

                        449  Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3

                              Split, 447

 

                       

                        Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                       

                        Suppose...

 

                              450  (t,u,v) e q

                                    Premise

 

                              451  ALL(b):ALL(c):[(t,b,c) e q

                             <=> (t,b,c) e add & ~[t=x & b=next(y) & c=z']]

                                    U Spec, 445

 

                              452  ALL(c):[(t,u,c) e q

                             <=> (t,u,c) e add & ~[t=x & u=next(y) & c=z']]

                                    U Spec, 451

 

                              453  (t,u,v) e q

                             <=> (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    U Spec, 452

 

                              454  [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']]

                             & [(t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q]

                                    Iff-And, 453

 

                              455  (t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    Split, 454

 

                              456  (t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q

                                    Split, 454

 

                              457  (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    Detach, 455, 450

 

                              458  (t,u,v) e add

                                    Split, 457

 

                              459  ~[t=x & u=next(y) & v=z']

                                    Split, 457

 

                              460  ALL(b):ALL(c):[(t,b,c) e add

                             <=> (t,b,c) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,b,c) e d]]

                                    U Spec, 26

 

                              461  ALL(c):[(t,u,c) e add

                             <=> (t,u,c) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,c) e d]]

                                    U Spec, 460

 

                              462  (t,u,v) e add

                             <=> (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    U Spec, 461

 

                              463  [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]]

                             & [(t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d] => (t,u,v) e add]

                                    Iff-And, 462

 

                              464  (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    Split, 463

 

                              465  (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d] => (t,u,v) e add

                                    Split, 463

 

                              466  (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    Detach, 464, 458

 

                              467  (t,u,v) e n3

                                    Split, 466

 

                   As Required:

 

                        468  ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                              4 Conclusion, 450

 

                        469  Set''(q)

                        & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                              Join, 444, 468

 

                   As Required:

 

                        470  q e pn3

                              Detach, 449, 469

 

                       

                        Prove: ALL(e):[e e n => (e,0,e) e q]

                       

                        Suppose...

 

                              471  t e n

                                    Premise

 

                              472  ALL(b):ALL(c):[(t,b,c) e q

                             <=> (t,b,c) e add & ~[t=x & b=next(y) & c=z']]

                                    U Spec, 445

 

                              473  ALL(c):[(t,0,c) e q

                             <=> (t,0,c) e add & ~[t=x & 0=next(y) & c=z']]

                                    U Spec, 472

 

                              474  (t,0,t) e q

                             <=> (t,0,t) e add & ~[t=x & 0=next(y) & t=z']

                                    U Spec, 473

 

                              475  [(t,0,t) e q => (t,0,t) e add & ~[t=x & 0=next(y) & t=z']]

                             & [(t,0,t) e add & ~[t=x & 0=next(y) & t=z'] => (t,0,t) e q]

                                    Iff-And, 474

 

                              476  (t,0,t) e q => (t,0,t) e add & ~[t=x & 0=next(y) & t=z']

                                    Split, 475

 

                              477  (t,0,t) e add & ~[t=x & 0=next(y) & t=z'] => (t,0,t) e q

                                    Split, 475

 

                              478  t e n => (t,0,t) e add

                                    U Spec, 52

 

                              479  (t,0,t) e add

                                    Detach, 478, 471

 

                            

                             Prove: t=x & 0=next(y) & t=z'

                            

                             Suppose to the contrary...

 

                                    480  t=x & 0=next(y) & t=z'

                                          Premise

 

                                    481  t=x

                                          Split, 480

 

                                    482  0=next(y)

                                          Split, 480

 

                                    483  t=z'

                                          Split, 480

 

                                    484  y e n => ~next(y)=0

                                          U Spec, 5

 

                                    485  ~next(y)=0

                                          Detach, 484, 400

 

                                    486  ~0=next(y)

                                          Sym, 485

 

                             Obtain the contradiction...

 

                                    487  0=next(y) & ~0=next(y)

                                          Join, 482, 486

 

                        As Required:

 

                              488  ~[t=x & 0=next(y) & t=z']

                                    4 Conclusion, 480

 

                              489  (t,0,t) e add & ~[t=x & 0=next(y) & t=z']

                                    Join, 479, 488

 

                              490  (t,0,t) e q

                                    Detach, 477, 489

 

                   As Required:

 

                        491  ALL(e):[e e n => (e,0,e) e q]

                              4 Conclusion, 471

 

                       

                        Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                       

                        Suppose...

 

                              492  (t,u,v) e q

                                    Premise

 

                              493  ALL(b):ALL(c):[(t,b,c) e q

                             <=> (t,b,c) e add & ~[t=x & b=next(y) & c=z']]

                                    U Spec, 445

 

                              494  ALL(c):[(t,u,c) e q

                             <=> (t,u,c) e add & ~[t=x & u=next(y) & c=z']]

                                    U Spec, 493

 

                              495  (t,u,v) e q

                             <=> (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    U Spec, 494

 

                              496  [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']]

                             & [(t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q]

                                    Iff-And, 495

 

                              497  (t,u,v) e q => (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    Split, 496

 

                              498  (t,u,v) e add & ~[t=x & u=next(y) & v=z'] => (t,u,v) e q

                                    Split, 496

 

                              499  (t,u,v) e add & ~[t=x & u=next(y) & v=z']

                                    Detach, 497, 492

 

                              500  (t,u,v) e add

                                    Split, 499

 

                              501  ~[t=x & u=next(y) & v=z']

                                    Split, 499

 

                              502  ALL(b):ALL(c):[(t,b,c) e add

                             <=> (t,b,c) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,b,c) e d]]

                                    U Spec, 26

 

                              503  ALL(c):[(t,u,c) e add

                             <=> (t,u,c) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,c) e d]]

                                    U Spec, 502

 

                              504  (t,u,v) e add

                             <=> (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    U Spec, 503

 

                              505  [(t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]]

                             & [(t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d] => (t,u,v) e add]

                                    Iff-And, 504

 

                              506  (t,u,v) e add => (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    Split, 505

 

                              507  (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d] => (t,u,v) e add

                                    Split, 505

 

                              508  (t,u,v) e n3 & ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    Detach, 506, 500

 

                              509  (t,u,v) e n3

                                    Split, 508

 

                              510  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                    U Spec, 16

 

                              511  ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]

                                    U Spec, 510

 

                              512  (t,u,v) e n3 <=> t e n & u e n & v e n

                                    U Spec, 511

 

                              513  [(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, 512

 

                              514  (t,u,v) e n3 => t e n & u e n & v e n

                                    Split, 513

 

                              515  t e n & u e n & v e n => (t,u,v) e n3

                                    Split, 513

 

                              516  t e n & u e n & v e n

                                    Detach, 514, 509

 

                              517  t e n

                                    Split, 516

 

                              518  u e n

                                    Split, 516

 

                              519  v e n

                                    Split, 516

 

                              520  ALL(d):[d e pn3

                             & ALL(e):[e e n => (e,0,e) e d]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                             => (t,u,v) e d]

                                    Split, 508

 

                              521  ALL(b):ALL(c):[(t,b,c) e q

                             <=> (t,b,c) e add & ~[t=x & b=next(y) & c=z']]

                                    U Spec, 445

 

                              522  ALL(c):[(t,next(u),c) e q

                             <=> (t,next(u),c) e add & ~[t=x & next(u)=next(y) & c=z']]

                                    U Spec, 521

 

                              523  (t,next(u),next(v)) e q

                             <=> (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']

                                    U Spec, 522

 

                              524  [(t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']]

                             & [(t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) e q]

                                    Iff-And, 523

 

                              525  (t,next(u),next(v)) e q => (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z']

                                    Split, 524

 

                        Sufficient: (t,next(u),next(v)) e q

 

                              526  (t,next(u),next(v)) e add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) e q

                                    Split, 524

 

                              527  ALL(b):ALL(c):[t e n & b e n & c e n

                             => [(t,b,c) e add => (t,next(b),next(c)) e add]]

                                    U Spec, 100

 

                              528  ALL(c):[t e n & u e n & c e n

                             => [(t,u,c) e add => (t,next(u),next(c)) e add]]

                                    U Spec, 527

 

                              529  t e n & u e n & v e n

                             => [(t,u,v) e add => (t,next(u),next(v)) e add]

                                    U Spec, 528

 

                              530  (t,u,v) e add => (t,next(u),next(v)) e add

                                    Detach, 529, 516

 

                              531  (t,next(u),next(v)) e add

                                    Detach, 530, 500

 

                            

                             Prove: t=x & next(u)=next(y) & next(v)=z'

                            

                             Suppose to the contrary...

 

                                    532  t=x & next(u)=next(y) & next(v)=z'

                                          Premise

 

                                    533  t=x

                                          Split, 532

 

                                    534  next(u)=next(y)

                                          Split, 532

 

                                    535  next(v)=z'

                                          Split, 532

 

                                    536  ALL(b):[u e n & b e n => [next(u)=next(b) => u=b]]

                                          U Spec, 4

 

                                    537  u e n & y e n => [next(u)=next(y) => u=y]

                                          U Spec, 536

 

                                    538  u e n & y e n

                                          Join, 518, 400

 

                                    539  next(u)=next(y) => u=y

                                          Detach, 537, 538

 

                                    540  u=y

                                          Detach, 539, 534

 

                                    541  (x,u,v) e add

                                          Substitute, 533, 500

 

                                    542  (x,y,v) e add

                                          Substitute, 540, 541

 

                                    543  v e n => [(x,y,v) e add => z=v]

                                          U Spec, 424

 

                                    544  (x,y,v) e add => z=v

                                          Detach, 543, 519

 

                                    545  z=v

                                          Detach, 544, 542

 

                                    546  next(z)=z'

                                          Substitute, 545, 535

 

                                    547  z'=next(z)

                                          Sym, 546

 

                             Obtain the contradiction...

 

                                    548  ~z'=next(z) & z'=next(z)

                                          Join, 428, 547

 

                        As Required:

 

                              549  ~[t=x & next(u)=next(y) & next(v)=z']

                                    4 Conclusion, 532

 

                              550  (t,next(u),next(v)) e add

                             & ~[t=x & next(u)=next(y) & next(v)=z']

                                    Join, 531, 549

 

                              551  (t,next(u),next(v)) e q

                                    Detach, 526, 550

 

                   As Required:

 

                        552  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                              4 Conclusion, 492

 

                        553  ALL(b):ALL(c):[(x,b,c) e q

                        <=> (x,b,c) e add & ~[x=x & b=next(y) & c=z']]

                              U Spec, 445

 

                        554  ALL(c):[(x,next(y),c) e q

                        <=> (x,next(y),c) e add & ~[x=x & next(y)=next(y) & c=z']]

                              U Spec, 553

 

                        555  (x,next(y),z') e q

                        <=> (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']

                              U Spec, 554

 

                        556  [(x,next(y),z') e q => (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']]

                        & [(x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') e q]

                              Iff-And, 555

 

                        557  (x,next(y),z') e q => (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']

                              Split, 556

 

                        558  (x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') e q

                              Split, 556

 

                        559  ~[(x,next(y),z') e add & ~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') e q

                              Contra, 557

 

                        560  ~~[~(x,next(y),z') e add | ~~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') e q

                              DeMorgan, 559

 

                        561  ~(x,next(y),z') e add | ~~[x=x & next(y)=next(y) & z'=z'] => ~(x,next(y),z') e q

                              Rem DNeg, 560

 

                        562  ~(x,next(y),z') e add | x=x & next(y)=next(y) & z'=z' => ~(x,next(y),z') e q

                              Rem DNeg, 561

 

                        563  x=x

                              Reflex

 

                        564  next(y)=next(y)

                              Reflex

 

                        565  z'=z'

                              Reflex

 

                        566  x=x & next(y)=next(y)

                              Join, 563, 564

 

                        567  x=x & next(y)=next(y) & z'=z'

                              Join, 566, 565

 

                        568  ~(x,next(y),z') e add | x=x & next(y)=next(y) & z'=z'

                              Arb Or, 567

 

                   As Required:

 

                        569  ~(x,next(y),z') e q

                              Detach, 562, 568

 

                        570  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                              Join, 470, 491

 

                        571  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                              Join, 570, 552

 

                        572  q e pn3 & ALL(e):[e e n => (e,0,e) e q]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,next(f),next(g)) e q]

                        & ~(x,next(y),z') e q

                              Join, 571, 569

 

                        573  EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        & ~(x,next(y),z') e d]

                              E Gen, 572

 

                        574  ~(x,next(y),z') e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,0,e) e d]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

                        & ~(x,next(y),z') e d]

                              Arb Or, 573

 

                        575  ~(x,next(y),z') e add

                              Detach, 441, 574

 

                   Obtain the contradiction...

 

                        576  (x,next(y),z') e add & ~(x,next(y),z') e add

                              Join, 427, 575

 

              As Required:

 

                  577  ~[(x,next(y),z') e add & ~z'=next(z)]

                        4 Conclusion, 426

 

                  578  ~~[(x,next(y),z') e add => ~~z'=next(z)]

                        Imply-And, 577

 

                  579  (x,next(y),z') e add => ~~z'=next(z)

                        Rem DNeg, 578

 

                  580  (x,next(y),z') e add => z'=next(z)

                        Rem DNeg, 579

 

          As Required:

 

            581  ALL(c'):[c' e n => [(x,next(y),c') e add => c'=next(z)]]

                  4 Conclusion, 425

 

             

              Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n

                     => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]

             

              Suppose...

 

                  582  z1 e n & z2 e n

                        Premise

 

                  583  z1 e n

                        Split, 582

 

                  584  z2 e n

                        Split, 582

 

                  

                   Prove: (x,next(y),z1) e add & (x,next(y),z2) e add => z1=z2

                  

                   Suppose...

 

                        585  (x,next(y),z1) e add & (x,next(y),z2) e add

                              Premise

 

                        586  (x,next(y),z1) e add

                              Split, 585

 

                        587  (x,next(y),z2) e add

                              Split, 585

 

                        588  z1 e n => [(x,next(y),z1) e add => z1=next(z)]

                              U Spec, 581

 

                        589  (x,next(y),z1) e add => z1=next(z)

                              Detach, 588, 583

 

                        590  z1=next(z)

                              Detach, 589, 586

 

                        591  z2 e n => [(x,next(y),z2) e add => z2=next(z)]

                              U Spec, 581

 

                        592  (x,next(y),z2) e add => z2=next(z)

                              Detach, 591, 584

 

                        593  z2=next(z)

                              Detach, 592, 587

 

                        594  z1=z2

                              Substitute, 593, 590

 

              As Required:

 

                  595  (x,next(y),z1) e add & (x,next(y),z2) e add => z1=z2

                        4 Conclusion, 585

 

          As Required:

 

            596  ALL(c1):ALL(c2):[c1 e n & c2 e n

              => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]

                  4 Conclusion, 582

 

            597  next(y) e n

              & ALL(c1):ALL(c2):[c1 e n & c2 e n

              => [(x,next(y),c1) e add & (x,next(y),c2) e add => c1=c2]]

                  Join, 407, 596

 

            598  next(y) e p2

                  Detach, 405, 597

 

     As Required:

 

      599  ALL(b):[b e p2 => next(b) e p2]

            4 Conclusion, 394

 

      600  0 e p2 & ALL(b):[b e p2 => next(b) e p2]

            Join, 393, 599

 

     As Required:

 

      601  ALL(b):[b e n => b e p2]

            Detach, 370, 600

 

         

          Prove: ALL(b):[b e n

                 => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

         

          Suppose...

 

            602  y e n

                  Premise

 

            603  y e n => y e p2

                  U Spec, 601

 

            604  y e p2

                  Detach, 603, 602

 

            605  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  U Spec, 359

 

            606  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]]

              & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2]

                  Iff-And, 605

 

            607  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Split, 606

 

            608  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]] => y e p2

                  Split, 606

 

            609  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Detach, 607, 604

 

            610  y e n

                  Split, 609

 

            611  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

                  Split, 609

 

     As Required:

 

      612  ALL(b):[b e n

          => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

            4 Conclusion, 602

 

As Required:

 

613  ALL(a):[a e n

     => ALL(b):[b e n

     => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e add & (a,b,c2) e add => c1=c2]]]]

      4 Conclusion, 355

 

    

     Prove: ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

    

     Suppose...

 

      614  (x,y,z1) e add & (x,y,z2) e add

            Premise

 

      615  (x,y,z1) e add

            Split, 614

 

      616  (x,y,z2) e add

            Split, 614

 

      617  ALL(b):ALL(c):[(x,b,c) e add

          <=> (x,b,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,b,c) e d]]

            U Spec, 26

 

      618  ALL(c):[(x,y,c) e add

          <=> (x,y,c) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,c) e d]]

            U Spec, 617

 

      619  (x,y,z1) e add

          <=> (x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d]

            U Spec, 618

 

      620  [(x,y,z1) e add => (x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d]]

          & [(x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d] => (x,y,z1) e add]

            Iff-And, 619

 

      621  (x,y,z1) e add => (x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d]

            Split, 620

 

      622  (x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d] => (x,y,z1) e add

            Split, 620

 

      623  (x,y,z1) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d]

            Detach, 621, 615

 

      624  (x,y,z1) e n3

            Split, 623

 

      625  ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z1) e d]

            Split, 623

 

      626  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 16

 

      627  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

            U Spec, 626

 

      628  (x,y,z1) e n3 <=> x e n & y e n & z1 e n

            U Spec, 627

 

      629  [(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, 628

 

      630  (x,y,z1) e n3 => x e n & y e n & z1 e n

            Split, 629

 

      631  x e n & y e n & z1 e n => (x,y,z1) e n3

            Split, 629

 

      632  x e n & y e n & z1 e n

            Detach, 630, 624

 

      633  x e n

            Split, 632

 

      634  y e n

            Split, 632

 

      635  z1 e n

            Split, 632

 

      636  (x,y,z2) e add

          <=> (x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d]

            U Spec, 618

 

      637  [(x,y,z2) e add => (x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d]]

          & [(x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d] => (x,y,z2) e add]

            Iff-And, 636

 

      638  (x,y,z2) e add => (x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d]

            Split, 637

 

      639  (x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d] => (x,y,z2) e add

            Split, 637

 

      640  (x,y,z2) e n3 & ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d]

            Detach, 638, 616

 

      641  (x,y,z2) e n3

            Split, 640

 

      642  ALL(d):[d e pn3

          & ALL(e):[e e n => (e,0,e) e d]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,next(f),next(g)) e d]

          => (x,y,z2) e d]

            Split, 640

 

      643  (x,y,z2) e n3 <=> x e n & y e n & z2 e n

            U Spec, 627

 

      644  [(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, 643

 

      645  (x,y,z2) e n3 => x e n & y e n & z2 e n

            Split, 644

 

      646  x e n & y e n & z2 e n => (x,y,z2) e n3

            Split, 644

 

      647  x e n & y e n & z2 e n

            Detach, 645, 641

 

      648  x e n

            Split, 647

 

      649  y e n

            Split, 647

 

      650  z2 e n

            Split, 647

 

      651  x e n

          => ALL(b):[b e n

          => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

            U Spec, 613

 

      652  ALL(b):[b e n

          => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e add & (x,b,c2) e add => c1=c2]]]

            Detach, 651, 633

 

      653  y e n

          => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

            U Spec, 652

 

      654  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e add & (x,y,c2) e add => c1=c2]]

            Detach, 653, 634

 

      655  ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e add & (x,y,c2) e add => z1=c2]]

            U Spec, 654

 

      656  z1 e n & z2 e n => [(x,y,z1) e add & (x,y,z2) e add => z1=z2]

            U Spec, 655

 

      657  z1 e n & z2 e n

            Join, 635, 650

 

      658  (x,y,z1) e add & (x,y,z2) e add => z1=z2

            Detach, 656, 657

 

      659  z1=z2

            Detach, 658, 614

 

As Required: Functionality, Part 3

 

660  ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

      4 Conclusion, 614

 

661  ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]

     & ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]

      Join, 270, 354

 

662  ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e add => c1 e n & c2 e n & c3 e n]

     & ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e add]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]

      Join, 661, 660

 

As Required: add is a function

 

663  ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]

      Detach, 252, 662

 

      664  x e n & y e n

            Premise

 

      665  x e n

            Split, 664

 

      666  y e n

            Split, 664

 

      667  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e add]]

            U Spec, 354

 

      668  x e n & y e n => EXIST(c):[c e n & (x,y,c) e add]

            U Spec, 667

 

      669  EXIST(c):[c e n & (x,y,c) e add]

            Detach, 668, 664

 

      670  z e n & (x,y,z) e add

            E Spec, 669

 

      671  z e n

            Split, 670

 

      672  (x,y,z) e add

            Split, 670

 

      673  ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]

            U Spec, 663

 

      674  ALL(d):[d=add(x,y) <=> (x,y,d) e add]

            U Spec, 673

 

      675  z=add(x,y) <=> (x,y,z) e add

            U Spec, 674

 

      676  [z=add(x,y) => (x,y,z) e add]

          & [(x,y,z) e add => z=add(x,y)]

            Iff-And, 675

 

      677  z=add(x,y) => (x,y,z) e add

            Split, 676

 

      678  (x,y,z) e add => z=add(x,y)

            Split, 676

 

      679  z=add(x,y)

            Detach, 678, 672

 

      680  add(x,y) e n

            Substitute, 679, 671

 

As Required:

 

681  ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]

      4 Conclusion, 664

 

    

     Prove: ALL(a):[a e n => add(a,0)=a]

    

     Suppose...

 

      682  x e n

            Premise

 

      683  x e n => (x,0,x) e add

            U Spec, 52

 

      684  (x,0,x) e add

            Detach, 683, 682

 

      685  ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]

            U Spec, 663

 

      686  ALL(d):[d=add(x,0) <=> (x,0,d) e add]

            U Spec, 685

 

      687  x=add(x,0) <=> (x,0,x) e add

            U Spec, 686

 

      688  [x=add(x,0) => (x,0,x) e add]

          & [(x,0,x) e add => x=add(x,0)]

            Iff-And, 687

 

      689  x=add(x,0) => (x,0,x) e add

            Split, 688

 

      690  (x,0,x) e add => x=add(x,0)

            Split, 688

 

      691  x=add(x,0)

            Detach, 690, 684

 

      692  add(x,0)=x

            Sym, 691

 

As Required:

 

693  ALL(a):[a e n => add(a,0)=a]

      4 Conclusion, 682

 

    

     Prove: ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]

    

     Suppose...

 

      694  x e n & y e n

            Premise

 

      695  x e n

            Split, 694

 

      696  y e n

            Split, 694

 

      697  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e add]]

            U Spec, 354

 

      698  x e n & y e n => EXIST(c):[c e n & (x,y,c) e add]

            U Spec, 697

 

      699  EXIST(c):[c e n & (x,y,c) e add]

            Detach, 698, 694

 

      700  z e n & (x,y,z) e add

            E Spec, 699

 

      701  z e n

            Split, 700

 

      702  (x,y,z) e add

            Split, 700

 

      703  ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]

            U Spec, 663

 

      704  ALL(d):[d=add(x,y) <=> (x,y,d) e add]

            U Spec, 703

 

      705  z=add(x,y) <=> (x,y,z) e add

            U Spec, 704

 

      706  [z=add(x,y) => (x,y,z) e add]

          & [(x,y,z) e add => z=add(x,y)]

            Iff-And, 705

 

      707  z=add(x,y) => (x,y,z) e add

            Split, 706

 

      708  (x,y,z) e add => z=add(x,y)

            Split, 706

 

      709  z=add(x,y)

            Detach, 708, 702

 

      710  ALL(b):ALL(c):[x e n & b e n & c e n

          => [(x,b,c) e add => (x,next(b),next(c)) e add]]

            U Spec, 100

 

      711  ALL(c):[x e n & y e n & c e n

          => [(x,y,c) e add => (x,next(y),next(c)) e add]]

            U Spec, 710

 

      712  x e n & y e n & z e n

          => [(x,y,z) e add => (x,next(y),next(z)) e add]

            U Spec, 711

 

      713  x e n & y e n & z e n

            Join, 694, 701

 

      714  (x,y,z) e add => (x,next(y),next(z)) e add

            Detach, 712, 713

 

      715  (x,next(y),next(z)) e add

            Detach, 714, 702

 

      716  ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]

            U Spec, 663

 

      717  ALL(d):[d=add(x,next(y)) <=> (x,next(y),d) e add]

            U Spec, 716

 

      718  next(z)=add(x,next(y)) <=> (x,next(y),next(z)) e add

            U Spec, 717

 

      719  [next(z)=add(x,next(y)) => (x,next(y),next(z)) e add]

          & [(x,next(y),next(z)) e add => next(z)=add(x,next(y))]

            Iff-And, 718

 

      720  next(z)=add(x,next(y)) => (x,next(y),next(z)) e add

            Split, 719

 

      721  (x,next(y),next(z)) e add => next(z)=add(x,next(y))

            Split, 719

 

      722  next(z)=add(x,next(y))

            Detach, 721, 715

 

      723  next(add(x,y))=add(x,next(y))

            Substitute, 709, 722

 

      724  add(x,next(y))=next(add(x,y))

            Sym, 723

 

As Required:

 

725  ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]

      4 Conclusion, 694

 

726  ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]

     & ALL(a):[a e n => add(a,0)=a]

      Join, 681, 693

 

727  ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]

     & ALL(a):[a e n => add(a,0)=a]

     & ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]

      Join, 726, 725

 

As Required:

 

728  EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]

     & ALL(a):[a e n => add(a,0)=a]

     & ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]]

      E Gen, 727