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