THEOREM

*******

For all x0 e N, there exists a function exp: NxN --> N such that, we have: 

 

   1. exp(0,0) = x0

   2. For all non-zero a, we have exp(a,0)=1    (starting with exponent 0)

   3. For all a, b e N, we have exp(a,b+1) = exp(a,b)*a

 

Where

  

   exp(x,y) = x to the power of y

 

 

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com 

 

Dan Christensen

2019-11-12

 

 

OUTLINE

*******

 

Lines    Content

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

 

1-13     Axioms/Definitions

 

14-36    Construct function exp: NxN --> N starting with exponent 0

 

37-943   Prove functionality of exp

 

944-1063 Establish required properties of the exp function

 

 

 

AXIOMS/DEFINITIONS

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

 

Define: n, 0, 1, 2

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

4     2 e n

      Axiom

 

5     2=1+1

      Axiom    

 

Properties of +

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

 

Closed on n

 

6     ALL(a):ALL(b):[a e n & b e n => a+b e n]

      Axiom

 

Right cancelability of +

 

7     ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]

      Axiom

 

0 is not the successor of any number

 

8     ALL(a):[a e n => ~a+1=0]

      Axiom

 

Principle of mathematical deduction using addition on n

 

9     ALL(a):[Set(a) & ALL(b):[b e a => b e n]

    => [0 e a & ALL(b):[b e a => b+1 e a]

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

      Axiom

 

Properties of *

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

 

Closed on n

 

10   ALL(a):ALL(b):[a e n & b e n => a*b e n]

      Axiom

 

11   ALL(a):[a e n => a*0=0]

      Axiom

 

12   ALL(a):[a e n => a*1=a]

      Axiom

 

13   ALL(a):ALL(b):[a e n & b e n => a*b=b*a]

      Axiom

 

   

    CONSTRUCT exp FUNCTION

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

   

    Suppose...

 

      14   x0 e n

            Premise

 

    Construct n2

 

      15   ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

            Cart Prod

 

      16   ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]

            U Spec, 15

 

      17   Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

            U Spec, 16

 

      18   Set(n) & Set(n)

            Join, 1, 1

 

      19   EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

            Detach, 17, 18

 

      20   Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

            E Spec, 19

 

    Define: n2

 

      21   Set'(n2)

            Split, 20

 

      22   ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

            Split, 20

 

    Construct n3

 

      23   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

 

      24   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, 23

 

      25   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, 24

 

      26   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, 25

 

      27   Set(n) & Set(n)

            Join, 1, 1

 

      28   Set(n) & Set(n) & Set(n)

            Join, 27, 1

 

      29   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, 26, 28

 

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

            E Spec, 29

 

    Define: n3

 

      31   Set''(n3)

            Split, 30

 

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

            Split, 30

 

    Construct exp

 

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

         <=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            Subset, 31

 

      34   Set''(exp) & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp

         <=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            E Spec, 33

 

   

    Define: exp

 

      35   Set''(exp)

            Split, 34

 

      36   ALL(a):ALL(b):ALL(c):[(a,b,c) e exp

         <=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            Split, 34

 

   

    PROVE FUNCTIONALITIY OF exp

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

   

    Apply Function Axiom

 

      37   ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e f]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

         => [(a1,a2,b1) e f & (a1,a2,b2) e f => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=> (a1,a2,b) e f]]]]

            Function

 

      38   ALL(dom):ALL(cod):[Set''(exp) & Set'(dom) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e dom & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e exp]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]]]

            U Spec, 37

 

      39   ALL(cod):[Set''(exp) & Set'(n2) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e cod & (a1,a2,b) e exp]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e cod & b2 e cod

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e cod => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]]]

            U Spec, 38

 

      40   Set''(exp) & Set'(n2) & Set(n)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e exp]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]]

            U Spec, 39

 

      41   Set''(exp) & Set'(n2)

            Join, 35, 21

 

      42   Set''(exp) & Set'(n2) & Set(n)

            Join, 41, 1

 

   

    Sufficient: For functionality of exp

 

      43   ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e exp]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]

            Detach, 40, 42

 

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

        

         Suppose...

 

            44   (x,y,z) e exp

                  Premise

 

            45   ALL(b):ALL(c):[(x,b,c) e exp

             <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  U Spec, 36

 

            46   ALL(c):[(x,y,c) e exp

             <=> (x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  U Spec, 45

 

            47   (x,y,z) e exp

             <=> (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  U Spec, 46

 

            48   [(x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

             & [(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  Iff-And, 47

 

            49   (x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  Split, 48

 

            50   (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  Split, 48

 

            51   (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  Detach, 49, 44

 

            52   (x,y,z) e n3

                  Split, 51

 

            53   ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                  Split, 51

 

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

                  U Spec, 32

 

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

                  U Spec, 54

 

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

                  U Spec, 55

 

            57   [(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, 56

 

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

                  Split, 57

 

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

                  Split, 57

 

            60   x e n & y e n & z e n

                  Detach, 58, 52

 

    As Required:

 

      61   ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => a e n & b e n & c e n]

            4 Conclusion, 44

 

      62   ALL(b):ALL(c):[(0,b,c) e exp

         <=> (0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            U Spec, 36

 

      63   ALL(c):[(0,0,c) e exp

         <=> (0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            U Spec, 62

 

      64   (0,0,x0) e exp

         <=> (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            U Spec, 63

 

      65   [(0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

         & [(0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

         => (0,0,x0) e d] => (0,0,x0) e exp]

            Iff-And, 64

 

      66   (0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            Split, 65

 

    Sufficient: For (0,0,x0) e exp

 

      67   (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

         => (0,0,x0) e d] => (0,0,x0) e exp

            Split, 65

 

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

            U Spec, 32

 

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

            U Spec, 68

 

      70   (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n

            U Spec, 69

 

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

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

            Iff-And, 70

 

      72   (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n

            Split, 71

 

      73   0 e n & 0 e n & x0 e n => (0,0,x0) e n3

            Split, 71

 

      74   0 e n & 0 e n

            Join, 2, 2

 

      75   0 e n & 0 e n & x0 e n

            Join, 74, 14

 

      76   (0,0,x0) e n3

            Detach, 73, 75

 

            77   Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

             & (0,0,x0) e d

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

             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                  Premise

 

            78   Set''(d)

                  Split, 77

 

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

                  Split, 77

 

            80   (0,0,x0) e d

                  Split, 77

 

      81   ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            4 Conclusion, 77

 

      82   (0,0,x0) e n3

         & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

         & (0,0,x0) e d

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

         & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

            Join, 76, 81

 

    As Required:

 

      83   (0,0,x0) e exp

            Detach, 67, 82

 

         Prove: ALL(a):[a e n => [~a=0 => (a,0,1) e exp]]

        

         Suppose...

 

            84   x e n

                  Premise

 

             Prove: ~x=0 => (x,0,1) e exp

            

             Suppose...

 

                  85   ~x=0

                        Premise

 

                  86   ALL(b):ALL(c):[(x,b,c) e exp

                 <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 36

 

                  87   ALL(c):[(x,0,c) e exp

                 <=> (x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 86

 

                  88   (x,0,1) e exp

                 <=> (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 87

 

                  89   [(x,0,1) e exp => (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                 & [(x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Iff-And, 88

 

                  90   (x,0,1) e exp => (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 89

 

             Sufficient: For (x,0,1) e exp

 

                  91   (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 89

 

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

                        U Spec, 32

 

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

                        U Spec, 92

 

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

                        U Spec, 93

 

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

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

                        Iff-And, 94

 

                  96   (x,0,1) e n3 => x e n & 0 e n & 1 e n

                        Split, 95

 

                  97   x e n & 0 e n & 1 e n => (x,0,1) e n3

                        Split, 95

 

                  98   x e n & 0 e n

                        Join, 84, 2

 

                  99   x e n & 0 e n & 1 e n

                        Join, 98, 3

 

                  100  (x,0,1) e n3

                        Detach, 97, 99

 

                        101  Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                              Premise

 

                        102  Set''(d)

                              Split, 101

 

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

                              Split, 101

 

                        104  (0,0,x0) e d

                              Split, 101

 

                        105  ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                              Split, 101

 

                        106  ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                              Split, 101

 

                        107  x e n => [~x=0 => (x,0,1) e d]

                              U Spec, 105

 

                        108  ~x=0 => (x,0,1) e d

                              Detach, 107, 84

 

                        109  (x,0,1) e d

                              Detach, 108, 85

 

                  110  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        4 Conclusion, 101

 

                  111  (x,0,1) e n3

                 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Join, 100, 110

 

                  112  (x,0,1) e exp

                        Detach, 91, 111

 

         As Required:

 

            113  ~x=0 => (x,0,1) e exp

                  4 Conclusion, 85

 

    As Required:

 

      114  ALL(a):[a e n => [~a=0 => (a,0,1) e exp]]

            4 Conclusion, 84

 

         Suppose...

 

            115  x e n & y e n & z e n

                  Premise

 

            116  x e n

                  Split, 115

 

            117  y e n

                  Split, 115

 

            118  z e n

                  Split, 115

 

             Suppose...

 

                  119  (x,y,z) e exp

                        Premise

 

                  120  ALL(b):ALL(c):[(x,b,c) e exp

                 <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 36

 

                  121  ALL(c):[(x,y,c) e exp

                 <=> (x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 120

 

                  122  (x,y,z) e exp

                 <=> (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 121

 

                  123  [(x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                 & [(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Iff-And, 122

 

                  124  (x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 123

 

                  125  (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 123

 

                  126  (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Detach, 124, 119

 

                  127  (x,y,z) e n3

                        Split, 126

 

                  128  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 126

 

                  129  ALL(b):[y e n & b e n => y+b e n]

                        U Spec, 6

 

                  130  y e n & 1 e n => y+1 e n

                        U Spec, 129

 

                  131  y e n & 1 e n

                        Join, 117, 3

 

                  132  y+1 e n

                        Detach, 130, 131

 

                  133  ALL(b):[z e n & b e n => z*b e n]

                        U Spec, 10

 

                  134  z e n & x e n => z*x e n

                        U Spec, 133

 

                  135  z e n & x e n

                        Join, 118, 116

 

                  136  z*x e n

                        Detach, 134, 135

 

                  137  ALL(b):ALL(c):[(x,b,c) e exp

                 <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 36

 

                  138  ALL(c):[(x,y+1,c) e exp

                 <=> (x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 137, 132

 

                  139  (x,y+1,z*x) e exp

                 <=> (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d]

                        U Spec, 138, 136

 

                  140  [(x,y+1,z*x) e exp => (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d]]

                 & [(x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d] => (x,y+1,z*x) e exp]

                        Iff-And, 139

 

                  141  (x,y+1,z*x) e exp => (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d]

                        Split, 140

 

             Sufficient: For (x,y+1,z*x) e exp

 

                  142  (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d] => (x,y+1,z*x) e exp

                        Split, 140

 

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

                        U Spec, 32

 

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

                        U Spec, 143, 132

 

                  145  (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n

                        U Spec, 144, 136

 

                  146  [(x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n]

                 & [x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3]

                        Iff-And, 145

 

                  147  (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n

                        Split, 146

 

                  148  x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3

                        Split, 146

 

                  149  x e n & y+1 e n

                        Join, 116, 132

 

                  150  x e n & y+1 e n & z*x e n

                        Join, 149, 136

 

                  151  (x,y+1,z*x) e n3

                        Detach, 148, 150

 

                        152  Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                              Premise

 

                        153  Set''(d)

                              Split, 152

 

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

                              Split, 152

 

                        155  (0,0,x0) e d

                              Split, 152

 

                        156  ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                              Split, 152

 

                        157  ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                              Split, 152

 

                        158  ALL(f):ALL(g):[(x,f,g) e d => (x,f+1,g*x) e d]

                              U Spec, 157

 

                        159  ALL(g):[(x,y,g) e d => (x,y+1,g*x) e d]

                              U Spec, 158

 

                        160  (x,y,z) e d => (x,y+1,z*x) e d

                              U Spec, 159

 

                        161  Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                      => (x,y,z) e d

                              U Spec, 128

 

                        162  (x,y,z) e d

                              Detach, 161, 152

 

                        163  (x,y+1,z*x) e d

                              Detach, 160, 162

 

                  164  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d]

                        4 Conclusion, 152

 

                  165  (x,y+1,z*x) e n3

                 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (x,y+1,z*x) e d]

                        Join, 151, 164

 

                  166  (x,y+1,z*x) e exp

                        Detach, 142, 165

 

            167  (x,y,z) e exp => (x,y+1,z*x) e exp

                  4 Conclusion, 119

 

    As Required:

 

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

         => [(a,b,c) e exp => (a,b+1,c*a) e exp]]

            4 Conclusion, 115

 

        

         Prove: ALL(c):[c e n => [(0,0,c) e exp => c=x0]]

        

         Suppose...

 

            169  z e n

                  Premise

 

            

             Prove: ~~[(0,0,z) e exp => z=x0]

            

             Suppose to the contrary...

 

                  170  ~[(0,0,z) e exp => z=x0]

                        Premise

 

                  171  ~~[(0,0,z) e exp & ~z=x0]

                        Imply-And, 170

 

                  172  (0,0,z) e exp & ~z=x0

                        Rem DNeg, 171

 

                  173  (0,0,z) e exp

                        Split, 172

 

                  174  ~z=x0

                        Split, 172

 

                  175  ALL(b):ALL(c):[(0,b,c) e exp

                 <=> (0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 36

 

                  176  ALL(c):[(0,0,c) e exp

                 <=> (0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 175

 

                  177  (0,0,z) e exp

                 <=> (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        U Spec, 176

 

                  178  [(0,0,z) e exp => (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                 & [(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Iff-And, 177

 

                  179  (0,0,z) e exp => (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 178

 

                  180  (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Split, 178

 

                  181  ~[(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (0,0,z) e d]] => ~(0,0,z) e exp

                        Contra, 179

 

                  182  ~~[~(0,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (0,0,z) e d]] => ~(0,0,z) e exp

                        DeMorgan, 181

 

                  183  ~(0,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (0,0,z) e d] => ~(0,0,z) e exp

                        Rem DNeg, 182

 

                  184  ~(0,0,z) e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (0,0,z) e d] => ~(0,0,z) e exp

                        Quant, 183

 

                  185  ~(0,0,z) e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                 => (0,0,z) e d] => ~(0,0,z) e exp

                        Rem DNeg, 184

 

                  186  ~(0,0,z) e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e exp

                        Imply-And, 185

 

             Sufficient: For ~(0,0,z) e exp  (to obtain a contradiction)

 

                  187  ~(0,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e exp

                        Rem DNeg, 186

 

             Construct q

 

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

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

                        Subset, 35

 

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

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

                        E Spec, 188

 

             Define: q

 

                  190  Set''(q)

                        Split, 189

 

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

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

                        Split, 189

 

                

                 Prove: ALL(d):ALL(e):ALL(f):[(d,e,f) e q => d e n & e e n & f e n]

                

                 Suppose...

 

                        192  (t,u,v) e q

                              Premise

 

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

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

                              U Spec, 191

 

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

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

                              U Spec, 193

 

                        195  (t,u,v) e q

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

                              U Spec, 194

 

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

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

                              Iff-And, 195

 

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

                              Split, 196

 

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

                              Split, 196

 

                        199  (t,u,v) e exp & ~[t=0 & u=0 & v=z]

                              Detach, 197, 192

 

                        200  (t,u,v) e exp

                              Split, 199

 

                        201  ~[t=0 & u=0 & v=z]

                              Split, 199

 

                        202  ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]

                              U Spec, 61

 

                        203  ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]

                              U Spec, 202

 

                        204  (t,u,v) e exp => t e n & u e n & v e n

                              U Spec, 203

 

                        205  t e n & u e n & v e n

                              Detach, 204, 200

 

             As Required:

 

                  206  ALL(d):ALL(e):ALL(f):[(d,e,f) e q => d e n & e e n & f e n]

                        4 Conclusion, 192

 

             As Required:

 

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

                        Rename, 206

 

                  208  ALL(b):ALL(c):[(0,b,c) e q

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

                        U Spec, 191

 

                  209  ALL(c):[(0,0,c) e q

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

                        U Spec, 208

 

                  210  (0,0,x0) e q

                 <=> (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

                        U Spec, 209

 

                  211  [(0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]]

                 & [(0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q]

                        Iff-And, 210

 

                  212  (0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

                        Split, 211

 

                  213  (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q

                        Split, 211

 

                        214  0=0 & 0=0 & x0=z

                              Premise

 

                        215  0=0

                              Split, 214

 

                        216  0=0

                              Split, 214

 

                        217  x0=z

                              Split, 214

 

                        218  z=x0

                              Sym, 217

 

                        219  z=x0 & ~z=x0

                              Join, 218, 174

 

                  220  ~[0=0 & 0=0 & x0=z]

                        4 Conclusion, 214

 

                  221  (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

                        Join, 83, 220

 

             As Required:

 

                  222  (0,0,x0) e q

                        Detach, 213, 221

 

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

                

                 Suppose...

 

                        223  x e n

                              Premise

 

                      Prove: ~x=0 => (x,0,1) e q

                     

                      Suppose...

 

                              224  ~x=0

                                    Premise

 

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

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

                                    U Spec, 191

 

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

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

                                    U Spec, 225

 

                              227  (x,0,1) e q

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

                                    U Spec, 226

 

                              228  [(x,0,1) e q => (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]]

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

                                    Iff-And, 227

 

                              229  (x,0,1) e q => (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]

                                    Split, 228

 

                              230  (x,0,1) e exp & ~[x=0 & 0=0 & 1=z] => (x,0,1) e q

                                    Split, 228

 

                              231  x e n => [~x=0 => (x,0,1) e exp]

                                    U Spec, 114

 

                              232  ~x=0 => (x,0,1) e exp

                                    Detach, 231, 223

 

                              233  (x,0,1) e exp

                                    Detach, 232, 224

 

                                    234  x=0 & 0=0 & 1=z

                                          Premise

 

                                    235  x=0

                                          Split, 234

 

                                    236  0=0

                                          Split, 234

 

                                    237  1=z

                                          Split, 234

 

                                    238  x=0 & ~x=0

                                          Join, 235, 224

 

                              239  ~[x=0 & 0=0 & 1=z]

                                    4 Conclusion, 234

 

                              240  (x,0,1) e exp & ~[x=0 & 0=0 & 1=z]

                                    Join, 233, 239

 

                              241  (x,0,1) e q

                                    Detach, 230, 240

 

                 As Required:

 

                        242  ~x=0 => (x,0,1) e q

                              4 Conclusion, 224

 

             As Required:

 

                  243  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        4 Conclusion, 223

 

                 Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                

                 Suppose...

 

                        244  (t,u,v) e q

                              Premise

 

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

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

                              U Spec, 191

 

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

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

                              U Spec, 245

 

                        247  (t,u,v) e q

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

                              U Spec, 246

 

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

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

                              Iff-And, 247

 

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

                              Split, 248

 

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

                              Split, 248

 

                        251  (t,u,v) e exp & ~[t=0 & u=0 & v=z]

                              Detach, 249, 244

 

                        252  (t,u,v) e exp

                              Split, 251

 

                        253  ~[t=0 & u=0 & v=z]

                              Split, 251

 

                        254  ALL(b):ALL(c):[(t,b,c) e exp

                      <=> (t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              U Spec, 36

 

                        255  ALL(c):[(t,u,c) e exp

                      <=> (t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              U Spec, 254

 

                        256  (t,u,v) e exp

                      <=> (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              U Spec, 255

 

                        257  [(t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                      & [(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              Iff-And, 256

 

                        258  (t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              Split, 257

 

                        259  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              Split, 257

 

                        260  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              Detach, 258, 252

 

                        261  (t,u,v) e n3

                              Split, 260

 

                        262  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                      & (0,0,x0) e d

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

                      & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                              Split, 260

 

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

                              U Spec, 32

 

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

                              U Spec, 263

 

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

                              U Spec, 264

 

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

 

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

                              Split, 266

 

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

                              Split, 266

 

                        269  t e n & u e n & v e n

                              Detach, 267, 261

 

                        270  t e n

                              Split, 269

 

                        271  u e n

                              Split, 269

 

                        272  v e n

                              Split, 269

 

                        273  ALL(b):[u e n & b e n => u+b e n]

                              U Spec, 6

 

                        274  u e n & 1 e n => u+1 e n

                              U Spec, 273

 

                        275  u e n & 1 e n

                              Join, 271, 3

 

                        276  u+1 e n

                              Detach, 274, 275

 

                        277  ALL(b):[v e n & b e n => v*b e n]

                              U Spec, 10

 

                        278  v e n & t e n => v*t e n

                              U Spec, 277

 

                        279  v e n & t e n

                              Join, 272, 270

 

                        280  v*t e n

                              Detach, 278, 279

 

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

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

                              U Spec, 191

 

                        282  ALL(c):[(t,u+1,c) e q

                      <=> (t,u+1,c) e exp & ~[t=0 & u+1=0 & c=z]]

                              U Spec, 281, 276

 

                        283  (t,u+1,v*t) e q

                      <=> (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

                              U Spec, 282, 280

 

                        284  [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]]

                      & [(t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q]

                              Iff-And, 283

 

                        285  (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

                              Split, 284

 

                 Sufficient: For (t,u+1,v*t) e q

 

                        286  (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q

                              Split, 284

 

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

                      => [(t,b,c) e exp => (t,b+1,c*t) e exp]]

                              U Spec, 168

 

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

                      => [(t,u,c) e exp => (t,u+1,c*t) e exp]]

                              U Spec, 287

 

                        289  t e n & u e n & v e n

                      => [(t,u,v) e exp => (t,u+1,v*t) e exp]

                              U Spec, 288

 

                        290  (t,u,v) e exp => (t,u+1,v*t) e exp

                              Detach, 289, 269

 

                        291  (t,u+1,v*t) e exp

                              Detach, 290, 252

 

                      Prove: ~[t=0 & u+1=0 & v*t=z]

                     

                      Suppose to the contrary...

 

                              292  t=0 & u+1=0 & v*t=z

                                    Premise

 

                              293  t=0

                                    Split, 292

 

                              294  u+1=0

                                    Split, 292

 

                              295  v*t=z

                                    Split, 292

 

                              296  u e n => ~u+1=0

                                    U Spec, 8

 

                              297  ~u+1=0

                                    Detach, 296, 271

 

                              298  u+1=0 & ~u+1=0

                                    Join, 294, 297

 

                 As Required:

 

                        299  ~[t=0 & u+1=0 & v*t=z]

                              4 Conclusion, 292

 

                        300  (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

                              Join, 291, 299

 

                        301  (t,u+1,v*t) e q

                              Detach, 286, 300

 

             As Required:

 

                  302  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                        4 Conclusion, 244

 

                  303  ALL(b):ALL(c):[(0,b,c) e q

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

                        U Spec, 191

 

                  304  ALL(c):[(0,0,c) e q

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

                        U Spec, 303

 

                  305  (0,0,z) e q

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

                        U Spec, 304

 

                  306  [(0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]]

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

                        Iff-And, 305

 

                  307  (0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]

                        Split, 306

 

                  308  (0,0,z) e exp & ~[0=0 & 0=0 & z=z] => (0,0,z) e q

                        Split, 306

 

                  309  ~[(0,0,z) e exp & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

                        Contra, 307

 

                  310  ~~[~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

                        DeMorgan, 309

 

                  311  ~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q

                        Rem DNeg, 310

 

                  312  ~(0,0,z) e exp | 0=0 & 0=0 & z=z => ~(0,0,z) e q

                        Rem DNeg, 311

 

                  313  0=0

                        Reflex

 

                  314  z=z

                        Reflex

 

                  315  0=0 & 0=0

                        Join, 313, 313

 

                  316  0=0 & 0=0 & z=z

                        Join, 315, 314

 

                  317  ~(0,0,z) e exp | 0=0 & 0=0 & z=z

                        Arb Or, 316

 

             As Required:

 

                  318  ~(0,0,z) e q

                        Detach, 312, 317

 

                  319  Set''(q)

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

                        Join, 190, 207

 

                  320  Set''(q)

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

                 & (0,0,x0) e q

                        Join, 319, 222

 

                  321  Set''(q)

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

                 & (0,0,x0) e q

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

                        Join, 320, 243

 

                  322  Set''(q)

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

                 & (0,0,x0) e q

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                        Join, 321, 302

 

                  323  Set''(q)

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

                 & (0,0,x0) e q

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                 & ~(0,0,z) e q

                        Join, 322, 318

 

                  324  EXIST(d):[Set''(d)

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

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        E Gen, 323

 

                  325  ~(0,0,z) e n3 | EXIST(d):[Set''(d)

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

                 & (0,0,x0) e d

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

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                        Arb Or, 324

 

                  326  ~(0,0,z) e exp

                        Detach, 187, 325

 

                  327  (0,0,z) e exp & ~(0,0,z) e exp

                        Join, 173, 326

 

         As Required:

 

            328  ~~[(0,0,z) e exp => z=x0]

                  4 Conclusion, 170

 

            329  (0,0,z) e exp => z=x0

                  Rem DNeg, 328

 

    As Required:

 

      330  ALL(c):[c e n => [(0,0,c) e exp => c=x0]]

            4 Conclusion, 169

 

        

         Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

        

         Suppose...

 

            331  (x,y,z) e exp

                  Premise

 

            332  ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n]

                  U Spec, 61

 

            333  ALL(c):[(x,y,c) e exp => x e n & y e n & c e n]

                  U Spec, 332

 

            334  (x,y,z) e exp => x e n & y e n & z e n

                  U Spec, 333

 

            335  x e n & y e n & z e n

                  Detach, 334, 331

 

            336  x e n

                  Split, 335

 

            337  y e n

                  Split, 335

 

            338  z e n

                  Split, 335

 

            339  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            340  (x,y) e n2 <=> x e n & y e n

                  U Spec, 339

 

            341  [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 340

 

            342  (x,y) e n2 => x e n & y e n

                  Split, 341

 

            343  x e n & y e n => (x,y) e n2

                  Split, 341

 

            344  x e n & y e n

                  Join, 336, 337

 

            345  (x,y) e n2

                  Detach, 343, 344

 

            346  (x,y) e n2 & z e n

                  Join, 345, 338

 

    Functionality, Part 1

 

      347  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

            4 Conclusion, 331

 

        

         Prove: ALL(a):[a e n

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

        

         Suppose...

 

            348  x e n

                  Premise

 

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

                  Subset, 1

 

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

                  E Spec, 349

 

        

         Define: p1

 

            351  Set(p1)

                  Split, 350

 

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

                  Split, 350

 

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

             => [0 e p1 & ALL(b):[b e p1 => b+1 e p1]

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

                  U Spec, 9

 

                  354  t e p1

                        Premise

 

                  355  t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e exp]

                        U Spec, 352

 

                  356  [t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e exp]]

                 & [t e n & EXIST(c):[c e n & (x,t,c) e exp] => t e p1]

                        Iff-And, 355

 

                  357  t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e exp]

                        Split, 356

 

                  358  t e n & EXIST(c):[c e n & (x,t,c) e exp] => t e p1

                        Split, 356

 

                  359  t e n & EXIST(c):[c e n & (x,t,c) e exp]

                        Detach, 357, 354

 

                  360  t e n

                        Split, 359

 

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

                  4 Conclusion, 354

 

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

                  Join, 351, 361

 

        

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

 

            363  0 e p1 & ALL(b):[b e p1 => b+1 e p1]

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

                  Detach, 353, 362

 

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

                  U Spec, 352

 

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

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

                  Iff-And, 364

 

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

                  Split, 365

 

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

                  Split, 365

 

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

                  U Spec, 352

 

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

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

                  Iff-And, 368

 

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

                  Split, 369

 

         Sufficient: For 0 e p1

 

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

                  Split, 369

 

         Two cases to consider:

 

            372  x=0 | ~x=0

                  Or Not

 

             Case 1

 

                  373  x=0

                        Premise

 

                  374  (x,0,x0) e exp

                        Substitute, 373, 83

 

                  375  x0 e n & (x,0,x0) e exp

                        Join, 14, 374

 

                  376  EXIST(c):[c e n & (x,0,c) e exp]

                        E Gen, 375

 

         As Required:

 

            377  x=0 => EXIST(c):[c e n & (x,0,c) e exp]

                  4 Conclusion, 373

 

             Case 2

            

             Prove: ~x=0 => EXIST(c):[c e n & (x,0,c) e exp]

            

             Suppose...

 

                  378  ~x=0

                        Premise

 

                  379  x e n => [~x=0 => (x,0,1) e exp]

                        U Spec, 114

 

                  380  ~x=0 => (x,0,1) e exp

                        Detach, 379, 348

 

                  381  (x,0,1) e exp

                        Detach, 380, 378

 

                  382  1 e n & (x,0,1) e exp

                        Join, 3, 381

 

                  383  EXIST(c):[c e n & (x,0,c) e exp]

                        E Gen, 382

 

         As Required:

 

            384  ~x=0 => EXIST(c):[c e n & (x,0,c) e exp]

                  4 Conclusion, 378

 

            385  [x=0 => EXIST(c):[c e n & (x,0,c) e exp]]

             & [~x=0 => EXIST(c):[c e n & (x,0,c) e exp]]

                  Join, 377, 384

 

            386  EXIST(c):[c e n & (x,0,c) e exp]

                  Cases, 372, 385

 

            387  0 e n & EXIST(c):[c e n & (x,0,c) e exp]

                  Join, 2, 386

 

         As Required:

 

            388  0 e p1

                  Detach, 371, 387

 

            

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

            

             Suppose...

 

                  389  y e p1

                        Premise

 

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

                        U Spec, 352

 

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

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

                        Iff-And, 390

 

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

                        Split, 391

 

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

                        Split, 391

 

                  394  y e n & EXIST(c):[c e n & (x,y,c) e exp]

                        Detach, 392, 389

 

                  395  y e n

                        Split, 394

 

                  396  EXIST(c):[c e n & (x,y,c) e exp]

                        Split, 394

 

                  397  z e n & (x,y,z) e exp

                        E Spec, 396

 

                  398  z e n

                        Split, 397

 

                  399  (x,y,z) e exp

                        Split, 397

 

                  400  ALL(b):[y e n & b e n => y+b e n]

                        U Spec, 6

 

                  401  y e n & 1 e n => y+1 e n

                        U Spec, 400

 

                  402  y e n & 1 e n

                        Join, 395, 3

 

                  403  y+1 e n

                        Detach, 401, 402

 

                  404  ALL(b):[z e n & b e n => z*b e n]

                        U Spec, 10

 

                  405  z e n & x e n => z*x e n

                        U Spec, 404

 

                  406  z e n & x e n

                        Join, 398, 348

 

                  407  z*x e n

                        Detach, 405, 406

 

                  408  y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

                        U Spec, 352, 403

 

                  409  [y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]]

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

                        Iff-And, 408

 

                  410  y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

                        Split, 409

 

             Sufficient:

 

                  411  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp] => y+1 e p1

                        Split, 409

 

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

                 => [(x,b,c) e exp => (x,b+1,c*x) e exp]]

                        U Spec, 168

 

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

                 => [(x,y,c) e exp => (x,y+1,c*x) e exp]]

                        U Spec, 412

 

                  414  x e n & y e n & z e n

                 => [(x,y,z) e exp => (x,y+1,z*x) e exp]

                        U Spec, 413

 

                  415  x e n & y e n

                        Join, 348, 395

 

                  416  x e n & y e n & z e n

                        Join, 415, 398

 

                  417  (x,y,z) e exp => (x,y+1,z*x) e exp

                        Detach, 414, 416

 

                  418  (x,y+1,z*x) e exp

                        Detach, 417, 399

 

                  419  z*x e n & (x,y+1,z*x) e exp

                        Join, 407, 418

 

                  420  EXIST(c):[c e n & (x,y+1,c) e exp]

                        E Gen, 419

 

                  421  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

                        Join, 403, 420

 

                  422  y+1 e p1

                        Detach, 411, 421

 

         As Required:

 

            423  ALL(b):[b e p1 => b+1 e p1]

                  4 Conclusion, 389

 

            424  0 e p1 & ALL(b):[b e p1 => b+1 e p1]

                  Join, 388, 423

 

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

                  Detach, 363, 424

 

            

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

            

             Suppose...

 

                  426  y e n

                        Premise

 

                  427  y e n => y e p1

                        U Spec, 425

 

                  428  y e p1

                        Detach, 427, 426

 

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

                        U Spec, 352

 

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

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

                        Iff-And, 429

 

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

                        Split, 430

 

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

                        Split, 430

 

                  433  y e n & EXIST(c):[c e n & (x,y,c) e exp]

                        Detach, 431, 428

 

                  434  y e n

                        Split, 433

 

                  435  EXIST(c):[c e n & (x,y,c) e exp]

                        Split, 433

 

         As Required:

 

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

                  4 Conclusion, 426

 

    As Required:

 

      437  ALL(a):[a e n

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

            4 Conclusion, 348

 

        

         Prove: ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]

        

         Suppose...

 

            438  (x,y) e n2

                  Premise

 

            439  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            440  (x,y) e n2 <=> x e n & y e n

                  U Spec, 439

 

            441  [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 440

 

            442  (x,y) e n2 => x e n & y e n

                  Split, 441

 

            443  x e n & y e n => (x,y) e n2

                  Split, 441

 

            444  x e n & y e n

                  Detach, 442, 438

 

            445  x e n

                  Split, 444

 

            446  y e n

                  Split, 444

 

            447  x e n

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

                  U Spec, 437

 

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

                  Detach, 447, 445

 

            449  y e n => EXIST(c):[c e n & (x,y,c) e exp]

                  U Spec, 448

 

            450  EXIST(c):[c e n & (x,y,c) e exp]

                  Detach, 449, 446

 

    Functionality, Part 2

 

      451  ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]

            4 Conclusion, 438

 

        

         Prove: ALL(a):[a e n

                => ALL(b):[b e n

                => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e exp & (a,b,c2) e exp => c1=c2]]]]

        

         Suppose...

 

            452  x e n

                  Premise

 

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

                  Subset, 1

 

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

                  E Spec, 453

 

        

         Define: p2

 

            455  Set(p2)

                  Split, 454

 

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

                  Split, 454

 

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

             => [0 e p2 & ALL(b):[b e p2 => b+1 e p2]

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

                  U Spec, 9

 

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

                  U Spec, 456

 

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

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

                  Iff-And, 458

 

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

                  Split, 459

 

         Sufficient:

 

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

                  Split, 459

 

            

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

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

            

             Suppose...

 

                  462  z1 e n & z2 e n

                        Premise

 

                  463  z1 e n

                        Split, 462

 

                  464  z2 e n

                        Split, 462

 

                

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

                

                 Suppose...

 

                        465  (x,0,z1) e exp & (x,0,z2) e exp

                              Premise

 

                        466  (x,0,z1) e exp

                              Split, 465

 

                        467  (x,0,z2) e exp

                              Split, 465

 

                 Two cases:

 

                        468  x=0 | ~x=0

                              Or Not

 

                      Case 1

                     

                      Prove: x=0 => z1=z2

                     

                      Suppose...

 

                              469  x=0

                                    Premise

 

                              470  (0,0,z1) e exp

                                    Substitute, 469, 466

 

                              471  (0,0,z2) e exp

                                    Substitute, 469, 467

 

                              472  z1 e n => [(0,0,z1) e exp => z1=x0]

                                    U Spec, 330

 

                              473  (0,0,z1) e exp => z1=x0

                                    Detach, 472, 463

 

                              474  z1=x0

                                    Detach, 473, 470

 

                              475  z2 e n => [(0,0,z2) e exp => z2=x0]

                                    U Spec, 330

 

                              476  (0,0,z2) e exp => z2=x0

                                    Detach, 475, 464

 

                              477  z2=x0

                                    Detach, 476, 471

 

                              478  z1=z2

                                    Substitute, 477, 474

 

                 As Required:

 

                        479  x=0 => z1=z2

                              4 Conclusion, 469

 

                      Case 2

                     

                      Prove: ~x=0 => z1=z2

                     

                      Suppose...

 

                              480  ~x=0

                                    Premise

 

                         

                          Prove: ALL(c):[c e n => [(x,0,c) e exp => c=1]]

                         

                          Suppose...

 

                                    481  z e n

                                          Premise

 

                               Suppose...

 

                                          482  ~[(x,0,z) e exp => z=1]

                                                Premise

 

                                          483  ~~[(x,0,z) e exp & ~z=1]

                                                Imply-And, 482

 

                                          484  (x,0,z) e exp & ~z=1

                                                Rem DNeg, 483

 

                                          485  (x,0,z) e exp

                                                Split, 484

 

                                          486  ~z=1

                                                Split, 484

 

                                          487  ALL(b):ALL(c):[(x,b,c) e exp

                                   <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                U Spec, 36

 

                                          488  ALL(c):[(x,0,c) e exp

                                   <=> (x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                U Spec, 487

 

                                          489  (x,0,z) e exp

                                   <=> (x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                U Spec, 488

 

                                          490  [(x,0,z) e exp => (x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                   & [(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Iff-And, 489

 

                                          491  (x,0,z) e exp => (x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Split, 490

 

                                          492  (x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Split, 490

 

                                          493  ~[(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Contra, 491

 

                                          494  ~~[~(x,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                DeMorgan, 493

 

                                          495  ~(x,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Rem DNeg, 494

 

                                          496  ~(x,0,z) e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Quant, 495

 

                                          497  ~(x,0,z) e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Rem DNeg, 496

 

                                          498  ~(x,0,z) e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e exp

                                                Imply-And, 497

 

                                          499  ~(x,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e exp

                                                Rem DNeg, 498

 

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

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

                                                Subset, 35

 

                                          501  Set''(q2) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q2

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

                                                E Spec, 500

 

                              

                               Define: q2

 

                                          502  Set''(q2)

                                                Split, 501

 

                                          503      ALL(a):ALL(b):ALL(c):[(a,b,c) e q2

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

                                                Split, 501

 

                                  

                                   Suppose...

 

                                                504  (t,u,v) e q2

                                                      Premise

 

                                                505      ALL(b):ALL(c):[(t,b,c) e q2

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

                                                      U Spec, 503

 

                                                506  ALL(c):[(t,u,c) e q2

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

                                                      U Spec, 505

 

                                                507  (t,u,v) e q2

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

                                                      U Spec, 506

 

                                                508  [(t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]]

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

                                                      Iff-And, 507

 

                                                509  (t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]

                                                      Split, 508

 

                                                510  (t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2

                                                      Split, 508

 

                                                511  (t,u,v) e exp & ~[t=x & u=0 & v=z]

                                                      Detach, 509, 504

 

                                                512  (t,u,v) e exp

                                                      Split, 511

 

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

                                                      Split, 511

 

                                                514      ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]

                                                      U Spec, 61

 

                                                515  ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]

                                                      U Spec, 514

 

                                                516  (t,u,v) e exp => t e n & u e n & v e n

                                                      U Spec, 515

 

                                                517  t e n & u e n & v e n

                                                      Detach, 516, 512

 

                               As Required:

 

                                          518      ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                                4 Conclusion, 504

 

                                          519  ALL(b):ALL(c):[(0,b,c) e q2

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

                                                U Spec, 503

 

                                          520  ALL(c):[(0,0,c) e q2

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

                                                U Spec, 519

 

                                          521  (0,0,x0) e q2

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

                                                U Spec, 520

 

                                          522  [(0,0,x0) e q2 => (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]]

                                   & [(0,0,x0) e exp & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q2]

                                                Iff-And, 521

 

                                          523  (0,0,x0) e q2 => (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]

                                                Split, 522

 

                              Sufficient:

 

                                          524  (0,0,x0) e exp & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q2

                                                Split, 522

 

                                                525  0=x & 0=0 & x0=z

                                                      Premise

 

                                                526  0=x

                                                      Split, 525

 

                                                527  0=0

                                                      Split, 525

 

                                                528  x0=z

                                                      Split, 525

 

                                                529  x=0

                                                      Sym, 526

 

                                                530  x=0 & ~x=0

                                                      Join, 529, 480

 

                                          531  ~[0=x & 0=0 & x0=z]

                                                4 Conclusion, 525

 

                                          532  (0,0,x0) e exp & ~[0=x & 0=0 & x0=z]

                                                Join, 83, 531

 

                               As Required:

 

                                          533  (0,0,x0) e q2

                                                Detach, 524, 532

 

                                                534  t e n

                                                      Premise

 

                                                      535  ~t=0

                                                            Premise

 

                                                      536      ALL(b):ALL(c):[(t,b,c) e q2

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

                                                            U Spec, 503

 

                                                      537  ALL(c):[(t,0,c) e q2

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

                                                            U Spec, 536

 

                                                      538  (t,0,1) e q2

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

                                                            U Spec, 537

 

                                                      539  [(t,0,1) e q2 => (t,0,1) e exp & ~[t=x & 0=0 & 1=z]]

                                            & [(t,0,1) e exp & ~[t=x & 0=0 & 1=z] => (t,0,1) e q2]

                                                            Iff-And, 538

 

                                                      540  (t,0,1) e q2 => (t,0,1) e exp & ~[t=x & 0=0 & 1=z]

                                                            Split, 539

 

                                       Sufficient:

 

                                                      541  (t,0,1) e exp & ~[t=x & 0=0 & 1=z] => (t,0,1) e q2

                                                            Split, 539

 

                                                      542  t e n => [~t=0 => (t,0,1) e exp]

                                                            U Spec, 114

 

                                                      543  ~t=0 => (t,0,1) e exp

                                                            Detach, 542, 534

 

                                                      544  (t,0,1) e exp

                                                            Detach, 543, 535

 

                                                            545  t=x & 0=0 & 1=z

                                                                  Premise

 

                                                            546  t=x

                                                                  Split, 545

 

                                                            547  0=0

                                                                  Split, 545

 

                                                            548  1=z

                                                                  Split, 545

 

                                                            549  z=1

                                                                  Sym, 548

 

                                                            550  z=1 & ~z=1

                                                                  Join, 549, 486

 

                                                      551  ~[t=x & 0=0 & 1=z]

                                                            4 Conclusion, 545

 

                                                      552  (t,0,1) e exp & ~[t=x & 0=0 & 1=z]

                                                            Join, 544, 551

 

                                                      553  (t,0,1) e q2

                                                            Detach, 541, 552

 

                                                554  ~t=0 => (t,0,1) e q2

                                                      4 Conclusion, 535

 

                               As Required:

 

                                          555  ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]

                                                4 Conclusion, 534

 

                                  

                                   Suppose...

 

                                                556  (t,u,v) e q2

                                                      Premise

 

                                                557      ALL(b):ALL(c):[(t,b,c) e q2

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

                                                      U Spec, 503

 

                                                558  ALL(c):[(t,u,c) e q2

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

                                                      U Spec, 557

 

                                                559  (t,u,v) e q2

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

                                                      U Spec, 558

 

                                                560  [(t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]]

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

                                                      Iff-And, 559

 

                                                561  (t,u,v) e q2 => (t,u,v) e exp & ~[t=x & u=0 & v=z]

                                                      Split, 560

 

                                                562  (t,u,v) e exp & ~[t=x & u=0 & v=z] => (t,u,v) e q2

                                                      Split, 560

 

                                                563  (t,u,v) e exp & ~[t=x & u=0 & v=z]

                                                      Detach, 561, 556

 

                                                564  (t,u,v) e exp

                                                      Split, 563

 

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

                                                      Split, 563

 

                                                566      ALL(b):ALL(c):[(t,b,c) e exp

                                       <=> (t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      U Spec, 36

 

                                                567  ALL(c):[(t,u,c) e exp

                                       <=> (t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      U Spec, 566

 

                                                568  (t,u,v) e exp

                                       <=> (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      U Spec, 567

 

                                                569  [(t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                       & [(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      Iff-And, 568

 

                                                570  (t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      Split, 569

 

                                                571  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      Split, 569

 

                                                572  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      Detach, 570, 564

 

                                                573  (t,u,v) e n3

                                                      Split, 572

 

                                                574  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                                       & (0,0,x0) e d

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

                                       & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                      Split, 572

 

                                                575      ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]

                                                      U Spec, 61

 

                                                576  ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]

                                                      U Spec, 575

 

                                                577  (t,u,v) e exp => t e n & u e n & v e n

                                                      U Spec, 576

 

                                                578  t e n & u e n & v e n

                                                      Detach, 577, 564

 

                                                579  t e n

                                                      Split, 578

 

                                                580  u e n

                                                      Split, 578

 

                                                581  v e n

                                                      Split, 578

 

                                                582  ALL(b):[u e n & b e n => u+b e n]

                                                      U Spec, 6

 

                                                583  u e n & 1 e n => u+1 e n

                                                      U Spec, 582

 

                                                584  u e n & 1 e n

                                                      Join, 580, 3

 

                                                585  u+1 e n

                                                      Detach, 583, 584

 

                                                586  ALL(b):[v e n & b e n => v*b e n]

                                                      U Spec, 10

 

                                                587  v e n & t e n => v*t e n

                                                      U Spec, 586

 

                                                588  v e n & t e n

                                                      Join, 581, 579

 

                                                589  v*t e n

                                                      Detach, 587, 588

 

                                                590      ALL(b):ALL(c):[(t,b,c) e q2

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

                                                      U Spec, 503

 

                                                591  ALL(c):[(t,u+1,c) e q2

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

                                                      U Spec, 590, 585

 

                                                592  (t,u+1,v*t) e q2

                                       <=> (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]

                                                      U Spec, 591, 589

 

                                                593  [(t,u+1,v*t) e q2 => (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]]

                                       & [(t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q2]

                                                      Iff-And, 592

 

                                                594  (t,u+1,v*t) e q2 => (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]

                                                      Split, 593

 

                                   Sufficient:

 

                                                595  (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q2

                                                      Split, 593

 

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

                                       => [(t,b,c) e exp => (t,b+1,c*t) e exp]]

                                                      U Spec, 168

 

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

                                       => [(t,u,c) e exp => (t,u+1,c*t) e exp]]

                                                      U Spec, 596

 

                                                598  t e n & u e n & v e n

                                       => [(t,u,v) e exp => (t,u+1,v*t) e exp]

                                                      U Spec, 597

 

                                                599  (t,u,v) e exp => (t,u+1,v*t) e exp

                                                      Detach, 598, 578

 

                                                600  (t,u+1,v*t) e exp

                                                      Detach, 599, 564

 

                                                      601  t=x & u+1=0 & v*t=z

                                                            Premise

 

                                                      602  t=x

                                                            Split, 601

 

                                                      603  u+1=0

                                                            Split, 601

 

                                                      604  v*t=z

                                                            Split, 601

 

                                                      605  u e n => ~u+1=0

                                                            U Spec, 8

 

                                                      606  ~u+1=0

                                                            Detach, 605, 580

 

                                                      607  u+1=0 & ~u+1=0

                                                            Join, 603, 606

 

                                                608  ~[t=x & u+1=0 & v*t=z]

                                                      4 Conclusion, 601

 

                                                609  (t,u+1,v*t) e exp & ~[t=x & u+1=0 & v*t=z]

                                                      Join, 600, 608

 

                                                610  (t,u+1,v*t) e q2

                                                      Detach, 595, 609

 

                               As Required:

 

                                          611      ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]

                                                4 Conclusion, 556

 

                                          612  ALL(b):ALL(c):[(x,b,c) e q2

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

                                                U Spec, 503

 

                                          613  ALL(c):[(x,0,c) e q2

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

                                                U Spec, 612

 

                                          614  (x,0,z) e q2

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

                                                U Spec, 613

 

                                          615  [(x,0,z) e q2 => (x,0,z) e exp & ~[x=x & 0=0 & z=z]]

                                   & [(x,0,z) e exp & ~[x=x & 0=0 & z=z] => (x,0,z) e q2]

                                                Iff-And, 614

 

                                          616  (x,0,z) e q2 => (x,0,z) e exp & ~[x=x & 0=0 & z=z]

                                                Split, 615

 

                                          617  (x,0,z) e exp & ~[x=x & 0=0 & z=z] => (x,0,z) e q2

                                                Split, 615

 

                                          618  ~[(x,0,z) e exp & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q2

                                                Contra, 616

 

                                          619  ~~[~(x,0,z) e exp | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q2

                                                DeMorgan, 618

 

                                          620  ~(x,0,z) e exp | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q2

                                                Rem DNeg, 619

 

                               Sufficient:

 

                                          621  ~(x,0,z) e exp | x=x & 0=0 & z=z => ~(x,0,z) e q2

                                                Rem DNeg, 620

 

                                          622  x=x

                                                Reflex

 

                                          623  0=0

                                                Reflex

 

                                          624  z=z

                                                Reflex

 

                                          625  x=x & 0=0

                                                Join, 622, 623

 

                                          626  x=x & 0=0 & z=z

                                                Join, 625, 624

 

                                          627  ~(x,0,z) e exp | x=x & 0=0 & z=z

                                                Arb Or, 626

 

                               As Required:

 

                                          628  ~(x,0,z) e q2

                                                Detach, 621, 627

 

                                          629  Set''(q2)

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                                Join, 502, 518

 

                                          630  Set''(q2)

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                   & (0,0,x0) e q2

                                                Join, 629, 533

 

                                          631  Set''(q2)

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                   & (0,0,x0) e q2

                                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]

                                                Join, 630, 555

 

                                          632  Set''(q2)

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                   & (0,0,x0) e q2

                                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]

                                                Join, 631, 611

 

                                          633  Set''(q2)

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]

                                   & (0,0,x0) e q2

                                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q2]]

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,f+1,g*e) e q2]

                                   & ~(x,0,z) e q2

                                                Join, 632, 628

 

                                          634  EXIST(d):[Set''(d)

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

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                E Gen, 633

 

                                          635  ~(x,0,z) e n3 | EXIST(d):[Set''(d)

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

                                   & (0,0,x0) e d

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

                                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                                Arb Or, 634

 

                                          636  ~(x,0,z) e exp

                                                Detach, 499, 635

 

                                          637  (x,0,z) e exp & ~(x,0,z) e exp

                                                Join, 485, 636

 

                                    638  ~~[(x,0,z) e exp => z=1]

                                          4 Conclusion, 482

 

                                    639  (x,0,z) e exp => z=1

                                          Rem DNeg, 638

 

                      As Required:

 

                              640  ALL(c):[c e n => [(x,0,c) e exp => c=1]]

                                    4 Conclusion, 481

 

                              641  z1 e n => [(x,0,z1) e exp => z1=1]

                                    U Spec, 640

 

                              642  (x,0,z1) e exp => z1=1

                                    Detach, 641, 463

 

                              643  z1=1

                                    Detach, 642, 466

 

                              644  z2 e n => [(x,0,z2) e exp => z2=1]

                                    U Spec, 640

 

                              645  (x,0,z2) e exp => z2=1

                                    Detach, 644, 464

 

                              646  z2=1

                                    Detach, 645, 467

 

                              647  z1=z2

                                    Substitute, 646, 643

 

                 As Required:

 

                        648  ~x=0 => z1=z2

                              4 Conclusion, 480

 

                        649  [x=0 => z1=z2] & [~x=0 => z1=z2]

                              Join, 479, 648

 

                        650  z1=z2

                              Cases, 468, 649

 

             As Required:

 

                  651  (x,0,z1) e exp & (x,0,z2) e exp => z1=z2

                        4 Conclusion, 465

 

         As Required:

 

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

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

                  4 Conclusion, 462

 

            653  0 e n

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

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

                  Join, 2, 652

 

         As Required:

 

            654  0 e p2

                  Detach, 461, 653

 

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

            

             Suppose...

 

                  655  t e p2

                        Premise

 

                  656  t e p2 <=> t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        U Spec, 456

 

                  657  [t e p2 => t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]]

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

                        Iff-And, 656

 

                  658  t e p2 => t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        Split, 657

 

                  659  t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2

                        Split, 657

 

                  660  t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        Detach, 658, 655

 

                  661  t e n

                        Split, 660

 

         As Required:

 

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

                  4 Conclusion, 655

 

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

                  Join, 455, 662

 

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

 

            664  0 e p2 & ALL(b):[b e p2 => b+1 e p2]

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

                  Detach, 457, 663

 

            

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

            

             Suppose...

 

                  665  y e p2

                        Premise

 

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

                        U Spec, 456

 

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

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

                        Iff-And, 666

 

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

                        Split, 667

 

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

                        Split, 667

 

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

                        Detach, 668, 665

 

                  671  y e n

                        Split, 670

 

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

                        Split, 670

 

                  673  ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]

                        U Spec, 451

 

                  674  (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]

                        U Spec, 673

 

                  675  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                        U Spec, 22

 

                  676  (x,y) e n2 <=> x e n & y e n

                        U Spec, 675

 

                  677  [(x,y) e n2 => x e n & y e n]

                 & [x e n & y e n => (x,y) e n2]

                        Iff-And, 676

 

                  678  (x,y) e n2 => x e n & y e n

                        Split, 677

 

                  679  x e n & y e n => (x,y) e n2

                        Split, 677

 

                  680  x e n & y e n

                        Join, 452, 671

 

                  681  (x,y) e n2

                        Detach, 679, 680

 

                  682  EXIST(c):[c e n & (x,y,c) e exp]

                        Detach, 674, 681

 

                  683  z e n & (x,y,z) e exp

                        E Spec, 682

 

                  684  z e n

                        Split, 683

 

                  685  (x,y,z) e exp

                        Split, 683

 

             688

 

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

                        U Spec, 672

 

                        687  z' e n

                              Premise

 

                        688  z e n & z' e n => [(x,y,z) e exp & (x,y,z') e exp => z=z']

                              U Spec, 686

 

                        689  z e n & z' e n

                              Join, 684, 687

 

                        690  (x,y,z) e exp & (x,y,z') e exp => z=z'

                              Detach, 688, 689

 

                              691  (x,y,z') e exp

                                    Premise

 

                              692  (x,y,z) e exp & (x,y,z') e exp

                                    Join, 685, 691

 

                              693  z=z'

                                    Detach, 690, 692

 

                        694  (x,y,z') e exp => z=z'

                              4 Conclusion, 691

 

                  695  ALL(c):[c e n => [(x,y,c) e exp => z=c]]

                        4 Conclusion, 687

 

                

                 Suppose...

 

                        696  z' e n

                              Premise

 

                     

                      Suppose to the contrary...

 

                              697  ~[(x,y+1,z') e exp => z'=z*x]

                                    Premise

 

                              698  ~~[(x,y+1,z') e exp & ~z'=z*x]

                                    Imply-And, 697

 

                              699  (x,y+1,z') e exp & ~z'=z*x

                                    Rem DNeg, 698

 

                              700  (x,y+1,z') e exp

                                    Split, 699

 

                              701  ~z'=z*x

                                    Split, 699

 

                              702  ALL(b):ALL(c):[(x,b,c) e exp

                          <=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                    U Spec, 36

 

                              703  ALL(b):[y e n & b e n => y+b e n]

                                    U Spec, 6

 

                              704  y e n & 1 e n => y+1 e n

                                    U Spec, 703

 

                              705  y e n & 1 e n

                                    Join, 671, 3

 

                              706  y+1 e n

                                    Detach, 704, 705

 

                              707  ALL(c):[(x,y+1,c) e exp

                          <=> (x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                    U Spec, 702, 706

 

                              708  (x,y+1,z') e exp

                          <=> (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                    U Spec, 707

 

                              709  [(x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                          & [(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d] => (x,y+1,z') e exp]

                                    Iff-And, 708

 

                              710  (x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                    Split, 709

 

                              711  (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d] => (x,y+1,z') e exp

                                    Split, 709

 

                              712  ~[(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d]] => ~(x,y+1,z') e exp

                                    Contra, 710

 

                              713  ~~[~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d]] => ~(x,y+1,z') e exp

                                    DeMorgan, 712

 

                              714  ~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d] => ~(x,y+1,z') e exp

                                    Rem DNeg, 713

 

                              715  ~(x,y+1,z') e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d] => ~(x,y+1,z') e exp

                                    Quant, 714

 

                              716  ~(x,y+1,z') e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z') e d] => ~(x,y+1,z') e exp

                                    Rem DNeg, 715

 

                              717  ~(x,y+1,z') e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e exp

                                    Imply-And, 716

 

                              718  ~(x,y+1,z') e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e exp

                                    Rem DNeg, 717

 

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

                          <=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]]

                                    Subset, 35

 

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

                          <=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]

                                    E Spec, 719

 

                      717

                     

                      Define: q

 

                              721  Set''(q)

                                    Split, 720

 

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

                          <=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]

                                    Split, 720

 

                                    723  (t,u,v) e q

                                          Premise

 

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

                               <=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 722

 

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

                               <=> (t,u,c) e exp & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 724

 

                                    726  (t,u,v) e q

                               <=> (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          U Spec, 725

 

                                    727  [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]

                               & [(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

                                          Iff-And, 726

 

                                    728  (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          Split, 727

 

                                    729  (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 727

 

                                    730  (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          Detach, 728, 723

 

                                    731  (t,u,v) e exp

                                          Split, 730

 

                                    732  ~[t=x & u=y+1 & v=z']

                                          Split, 730

 

                                    733  ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n]

                                          U Spec, 61

 

                                    734  ALL(c):[(t,u,c) e exp => t e n & u e n & c e n]

                                          U Spec, 733

 

                                    735  (t,u,v) e exp => t e n & u e n & v e n

                                          U Spec, 734

 

                                    736  t e n & u e n & v e n

                                          Detach, 735, 731

 

                      As Required:

 

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

                                    4 Conclusion, 723

 

                              738  ALL(b):ALL(c):[(0,b,c) e q

                          <=> (0,b,c) e exp & ~[0=x & b=y+1 & c=z']]

                                    U Spec, 722

 

                              739  ALL(c):[(0,0,c) e q

                          <=> (0,0,c) e exp & ~[0=x & 0=y+1 & c=z']]

                                    U Spec, 738

 

                              740  (0,0,x0) e q

                          <=> (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

                                    U Spec, 739

 

                              741  [(0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']]

                          & [(0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q]

                                    Iff-And, 740

 

                              742  (0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

                                    Split, 741

 

                      Sufficient:

 

                              743  (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q

                                    Split, 741

 

                                    744  0=x & 0=y+1 & x0=z'

                                          Premise

 

                                    745  0=x

                                          Split, 744

 

                                    746  0=y+1

                                          Split, 744

 

                                    747  x0=z'

                                          Split, 744

 

                                    748  y e n => ~y+1=0

                                          U Spec, 8

 

                                    749  ~y+1=0

                                          Detach, 748, 671

 

                                    750  y+1=0

                                          Sym, 746

 

                                    751  y+1=0 & ~y+1=0

                                          Join, 750, 749

 

                      As Required:

 

                              752  ~[0=x & 0=y+1 & x0=z']

                                    4 Conclusion, 744

 

                              753  (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

                                    Join, 83, 752

 

                      As Required:

 

                              754  (0,0,x0) e q

                                    Detach, 743, 753

 

                                    755  t e n

                                          Premise

 

                                          756  ~t=0

                                                Premise

 

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

                                   <=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

                                                U Spec, 722

 

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

                                   <=> (t,0,c) e exp & ~[t=x & 0=y+1 & c=z']]

                                                U Spec, 757

 

                                          759  (t,0,1) e q

                                   <=> (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

                                                U Spec, 758

 

                                          760  [(t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']]

                                   & [(t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q]

                                                Iff-And, 759

 

                                          761  (t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

                                                Split, 760

 

                               Sufficient:

 

                                          762  (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q

                                                Split, 760

 

                                          763  t e n => [~t=0 => (t,0,1) e exp]

                                                U Spec, 114

 

                                          764  ~t=0 => (t,0,1) e exp

                                                Detach, 763, 755

 

                                          765  (t,0,1) e exp

                                                Detach, 764, 756

 

                                                766  t=x & 0=y+1 & 1=z'

                                                      Premise

 

                                                767  t=x

                                                      Split, 766

 

                                                768  0=y+1

                                                      Split, 766

 

                                                769  1=z'

                                                      Split, 766

 

                                                770  y e n => ~y+1=0

                                                      U Spec, 8

 

                                                771  ~y+1=0

                                                      Detach, 770, 671

 

                                                772  ~0=y+1

                                                      Sym, 771

 

                                                773  0=y+1 & ~0=y+1

                                                      Join, 768, 772

 

                                          774  ~[t=x & 0=y+1 & 1=z']

                                                4 Conclusion, 766

 

                                          775  (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

                                                Join, 765, 774

 

                                          776  (t,0,1) e q

                                                Detach, 762, 775

 

                                    777  ~t=0 => (t,0,1) e q

                                          4 Conclusion, 756

 

                      As Required:

 

                              778  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                                    4 Conclusion, 755

 

                                    779  (t,u,v) e q

                                          Premise

 

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

                               <=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 722

 

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

                               <=> (t,u,c) e exp & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 780

 

                                    782  (t,u,v) e q

                               <=> (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          U Spec, 781

 

                                    783  [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]

                               & [(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

                                          Iff-And, 782

 

                                    784  (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          Split, 783

 

                                    785  (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 783

 

                                    786  (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

                                          Detach, 784, 779

 

                                    787  (t,u,v) e exp

                                          Split, 786

 

                                    788  ~[t=x & u=y+1 & v=z']

                                          Split, 786

 

                                    789  ALL(b):ALL(c):[(t,b,c) e exp

                               <=> (t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          U Spec, 36

 

                                    790  ALL(c):[(t,u,c) e exp

                               <=> (t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          U Spec, 789

 

                                    791  (t,u,v) e exp

                               <=> (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          U Spec, 790

 

                                    792  [(t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                               & [(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          Iff-And, 791

 

                                    793  (t,u,v) e exp => (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          Split, 792

 

                                    794  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          Split, 792

 

                                    795  (t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          Detach, 793, 787

 

                                    796  (t,u,v) e n3

                                          Split, 795

 

                                    797  ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

                               & (0,0,x0) e d

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

                               & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

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

                                          Split, 795

 

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

                                          U Spec, 32

 

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

                                          U Spec, 798

 

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

                                          U Spec, 799

 

                                    801  [(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, 800

 

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

                                          Split, 801

 

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

                                          Split, 801

 

                                    804  t e n & u e n & v e n

                                          Detach, 802, 796

 

                                    805  t e n

                                          Split, 804

 

                                    806  u e n

                                          Split, 804

 

                                    807  v e n

                                          Split, 804

 

                                    808  ALL(b):[u e n & b e n => u+b e n]

                                          U Spec, 6

 

                                    809  u e n & 1 e n => u+1 e n

                                          U Spec, 808

 

                                    810  u e n & 1 e n

                                          Join, 806, 3

 

                                    811  u+1 e n

                                          Detach, 809, 810

 

                                    812  ALL(b):[v e n & b e n => v*b e n]

                                          U Spec, 10

 

                                    813  v e n & t e n => v*t e n

                                          U Spec, 812

 

                                    814  v e n & t e n

                                          Join, 807, 805

 

                                    815  v*t e n

                                          Detach, 813, 814

 

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

                               <=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 722

 

                                    817  ALL(c):[(t,u+1,c) e q

                               <=> (t,u+1,c) e exp & ~[t=x & u+1=y+1 & c=z']]

                                          U Spec, 816, 811

 

                                    818  (t,u+1,v*t) e q

                               <=> (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

                                          U Spec, 817, 815

 

                                    819  [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']]

                               & [(t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q]

                                          Iff-And, 818

 

                                    820  (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

                                          Split, 819

 

                          Sufficient:

 

                                    821  (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q

                                          Split, 819

 

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

                               => [(t,b,c) e exp => (t,b+1,c*t) e exp]]

                                          U Spec, 168

 

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

                               => [(t,u,c) e exp => (t,u+1,c*t) e exp]]

                                          U Spec, 822

 

                                    824  t e n & u e n & v e n

                               => [(t,u,v) e exp => (t,u+1,v*t) e exp]

                                          U Spec, 823

 

                                    825  (t,u,v) e exp => (t,u+1,v*t) e exp

                                          Detach, 824, 804

 

                                    826  (t,u+1,v*t) e exp

                                          Detach, 825, 787

 

                                          827  t=x & u+1=y+1 & v*t=z'

                                                Premise

 

                                          828  t=x

                                                Split, 827

 

                                          829  u+1=y+1

                                                Split, 827

 

                                          830  v*t=z'

                                                Split, 827

 

                                          831  v*x=z'

                                                Substitute, 828, 830

 

                                          832  ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]

                                                U Spec, 7

 

                                          833  ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]

                                                U Spec, 832

 

                                          834  u e n & 1 e n & y e n => [u+1=y+1 => u=y]

                                                U Spec, 833

 

                                          835  u e n & 1 e n

                                                Join, 806, 3

 

                                          836  u e n & 1 e n & y e n

                                                Join, 835, 671

 

                                          837  u+1=y+1 => u=y

                                                Detach, 834, 836

 

                               829

 

                                          838  u=y

                                                Detach, 837, 829

 

                                          839  (x,u,v) e exp

                                                Substitute, 828, 787

 

                                          840  (x,y,v) e exp

                                                Substitute, 838, 839

 

                                          841  v e n => [(x,y,v) e exp => z=v]

                                                U Spec, 695

 

                                          842  (x,y,v) e exp => z=v

                                                Detach, 841, 807

 

                               834

 

                                          843  z=v

                                                Detach, 842, 840

 

                                          844  z*x=z'

                                                Substitute, 843, 831

 

                                          845  z'=z*x

                                                Sym, 844

 

                                          846  z'=z*x & ~z'=z*x

                                                Join, 845, 701

 

                                    847  ~[t=x & u+1=y+1 & v*t=z']

                                          4 Conclusion, 827

 

                                    848  (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

                                          Join, 826, 847

 

                                    849  (t,u+1,v*t) e q

                                          Detach, 821, 848

 

                              850  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    4 Conclusion, 779

 

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

                          <=> (x,b,c) e exp & ~[x=x & b=y+1 & c=z']]

                                    U Spec, 722

 

                              852  ALL(c):[(x,y+1,c) e q

                          <=> (x,y+1,c) e exp & ~[x=x & y+1=y+1 & c=z']]

                                    U Spec, 851, 706

 

                              853  (x,y+1,z') e q

                          <=> (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']

                                    U Spec, 852

 

                              854  [(x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']]

                          & [(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q]

                                    Iff-And, 853

 

                              855  (x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']

                                    Split, 854

 

                              856  (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q

                                    Split, 854

 

                              857  ~[(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    Contra, 855

 

                              858  ~~[~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    DeMorgan, 857

 

                              859  ~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q

                                    Rem DNeg, 858

 

                              860  ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q

                                    Rem DNeg, 859

 

                              861  x=x

                                    Reflex

 

                              862  y+1=y+1

                                    Reflex, 706

 

                              863  z'=z'

                                    Reflex

 

                              864  x=x & y+1=y+1

                                    Join, 861, 862

 

                              865  x=x & y+1=y+1 & z'=z'

                                    Join, 864, 863

 

                              866  ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z'

                                    Arb Or, 865

 

                      As Required:

 

                              867  ~(x,y+1,z') e q

                                    Detach, 860, 866

 

                              868  Set''(q)

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

                                    Join, 721, 737

 

                              869  Set''(q)

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

                          & (0,0,x0) e q

                                    Join, 868, 754

 

                              870  Set''(q)

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

                          & (0,0,x0) e q

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

                                    Join, 869, 778

 

                              871  Set''(q)

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

                          & (0,0,x0) e q

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    Join, 870, 850

 

                              872  Set''(q)

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

                          & (0,0,x0) e q

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                          & ~(x,y+1,z') e q

                                    Join, 871, 867

 

                              873  EXIST(d):[Set''(d)

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

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          & ~(x,y+1,z') e d]

                                    E Gen, 872

 

                              874  ~(x,y+1,z') e n3 | EXIST(d):[Set''(d)

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

                          & (0,0,x0) e d

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

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          & ~(x,y+1,z') e d]

                                    Arb Or, 873

 

                              875  ~(x,y+1,z') e exp

                                    Detach, 718, 874

 

                              876  ~(x,y+1,z') e exp & (x,y+1,z') e exp

                                    Join, 875, 700

 

                        877  ~~[(x,y+1,z') e exp => z'=z*x]

                              4 Conclusion, 697

 

                        878  (x,y+1,z') e exp => z'=z*x

                              Rem DNeg, 877

 

                  879  ALL(d):[d e n => [(x,y+1,d) e exp => d=z*x]]

                        4 Conclusion, 696

 

                  880  ALL(b):[y e n & b e n => y+b e n]

                        U Spec, 6

 

                  881  y e n & 1 e n => y+1 e n

                        U Spec, 880

 

                  882  y e n & 1 e n

                        Join, 671, 3

 

                  883  y+1 e n

                        Detach, 881, 882

 

                  884  y+1 e p2 <=> y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]

                        U Spec, 456, 883

 

                  885  [y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]]

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

                        Iff-And, 884

 

                  886  y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]

                        Split, 885

 

             Sufficient:

 

                  887  y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]] => y+1 e p2

                        Split, 885

 

                

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

                        => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]

                

                 Suppose...

 

                        888  z1 e n & z2 e n

                              Premise

 

                        889  z1 e n

                              Split, 888

 

                        890  z2 e n

                              Split, 888

 

                     

                      Prove: (x,y+1,z1) e exp & (x,y+1,z2) e exp => z1=z2

                     

                      Suppose...

 

                              891  (x,y+1,z1) e exp & (x,y+1,z2) e exp

                                    Premise

 

                              892  (x,y+1,z1) e exp

                                    Split, 891

 

                              893  (x,y+1,z2) e exp

                                    Split, 891

 

                              894  z1 e n => [(x,y+1,z1) e exp => z1=z*x]

                                    U Spec, 879

 

                              895  (x,y+1,z1) e exp => z1=z*x

                                    Detach, 894, 889

 

                              896  z1=z*x

                                    Detach, 895, 892

 

                              897  z2 e n => [(x,y+1,z2) e exp => z2=z*x]

                                    U Spec, 879

 

                              898  (x,y+1,z2) e exp => z2=z*x

                                    Detach, 897, 890

 

                              899  z2=z*x

                                    Detach, 898, 893

 

                              900  z1=z2

                                    Substitute, 899, 896

 

                 As Required:

 

                        901  (x,y+1,z1) e exp & (x,y+1,z2) e exp => z1=z2

                              4 Conclusion, 891

 

             As Required:

 

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

                 => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]

                        4 Conclusion, 888

 

                  903  y+1 e n

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

                 => [(x,y+1,c1) e exp & (x,y+1,c2) e exp => c1=c2]]

                        Join, 883, 902

 

                  904  y+1 e p2

                        Detach, 887, 903

 

         As Required:

 

            905  ALL(b):[b e p2 => b+1 e p2]

                  4 Conclusion, 665

 

            906  0 e p2 & ALL(b):[b e p2 => b+1 e p2]

                  Join, 654, 905

 

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

                  Detach, 664, 906

 

                  908  t e n

                        Premise

 

                  909  t e n => t e p2

                        U Spec, 907

 

                  910  t e p2

                        Detach, 909, 908

 

                  911  t e p2 <=> t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        U Spec, 456

 

                  912  [t e p2 => t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]]

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

                        Iff-And, 911

 

                  913  t e p2 => t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        Split, 912

 

                  914  t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]] => t e p2

                        Split, 912

 

                  915  t e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        Detach, 913, 910

 

                  916  t e n

                        Split, 915

 

                  917  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,t,c1) e exp & (x,t,c2) e exp => c1=c2]]

                        Split, 915

 

            918  ALL(b):[b e n

             => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]

                  4 Conclusion, 908

 

    As Required:

 

      919  ALL(a):[a e n

         => ALL(b):[b e n

         => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e exp & (a,b,c2) e exp => c1=c2]]]]

            4 Conclusion, 452

 

        

         Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n

                => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

        

         Suppose...

 

            920  (x,y) e n2 & z1 e n & z2 e n

                  Premise

 

            921  (x,y) e n2

                  Split, 920

 

            922  z1 e n

                  Split, 920

 

            923  z2 e n

                  Split, 920

 

            924  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            925  (x,y) e n2 <=> x e n & y e n

                  U Spec, 924

 

            926  [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 925

 

            927  (x,y) e n2 => x e n & y e n

                  Split, 926

 

            928  x e n & y e n => (x,y) e n2

                  Split, 926

 

            929  x e n & y e n

                  Detach, 927, 921

 

            930  x e n

                  Split, 929

 

            931  y e n

                  Split, 929

 

            932  x e n

             => ALL(b):[b e n

             => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]

                  U Spec, 919

 

            933  ALL(b):[b e n

             => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e exp & (x,b,c2) e exp => c1=c2]]]

                  Detach, 932, 930

 

            934  y e n

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

                  U Spec, 933

 

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

                  Detach, 934, 931

 

            936  ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e exp & (x,y,c2) e exp => z1=c2]]

                  U Spec, 935

 

            937  z1 e n & z2 e n => [(x,y,z1) e exp & (x,y,z2) e exp => z1=z2]

                  U Spec, 936

 

            938  z1 e n & z2 e n

                  Join, 922, 923

 

            939  (x,y,z1) e exp & (x,y,z2) e exp => z1=z2

                  Detach, 937, 938

 

    Functionality, Part 3

 

      940  ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

            4 Conclusion, 920

 

      941  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]

            Join, 347, 451

 

      942  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp => (a1,a2) e n2 & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e exp]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n

         => [(a1,a2,b1) e exp & (a1,a2,b2) e exp => b1=b2]]

            Join, 941, 940

 

   

    exp is a binary function on n

 

      943  ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n => [exp(a1,a2)=b <=> (a1,a2,b) e exp]]

            Detach, 43, 942

 

   

    ESTABLISH REQUIRED PROPERTIES OF exp

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

 

      944  ALL(a2):ALL(b):[(0,a2) e n2 & b e n => [exp(0,a2)=b <=> (0,a2,b) e exp]]

            U Spec, 943

 

      945  ALL(b):[(0,0) e n2 & b e n => [exp(0,0)=b <=> (0,0,b) e exp]]

            U Spec, 944

 

    Prove: exp(0,0)=x0

 

      946  (0,0) e n2 & x0 e n => [exp(0,0)=x0 <=> (0,0,x0) e exp]

            U Spec, 945

 

      947  ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]

            U Spec, 22

 

      948  (0,0) e n2 <=> 0 e n & 0 e n

            U Spec, 947

 

      949  [(0,0) e n2 => 0 e n & 0 e n]

         & [0 e n & 0 e n => (0,0) e n2]

            Iff-And, 948

 

      950  (0,0) e n2 => 0 e n & 0 e n

            Split, 949

 

      951  0 e n & 0 e n => (0,0) e n2

            Split, 949

 

      952  0 e n & 0 e n

            Join, 2, 2

 

      953  (0,0) e n2

            Detach, 951, 952

 

      954  (0,0) e n2 & x0 e n

            Join, 953, 14

 

      955  exp(0,0)=x0 <=> (0,0,x0) e exp

            Detach, 946, 954

 

      956  [exp(0,0)=x0 => (0,0,x0) e exp]

         & [(0,0,x0) e exp => exp(0,0)=x0]

            Iff-And, 955

 

      957  exp(0,0)=x0 => (0,0,x0) e exp

            Split, 956

 

      958  (0,0,x0) e exp => exp(0,0)=x0

            Split, 956

 

    As Required:

 

      959  exp(0,0)=x0

            Detach, 958, 83

 

        

         Prove: ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

        

         Suppose...

 

            960  x e n & y e n

                  Premise

 

            961  x e n

                  Split, 960

 

            962  y e n

                  Split, 960

 

            963  ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]

                  U Spec, 451

 

            964  (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]

                  U Spec, 963

 

            965  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            966  (x,y) e n2 <=> x e n & y e n

                  U Spec, 965

 

            967  [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 966

 

            968  (x,y) e n2 => x e n & y e n

                  Split, 967

 

            969  x e n & y e n => (x,y) e n2

                  Split, 967

 

            970  (x,y) e n2

                  Detach, 969, 960

 

            971  EXIST(c):[c e n & (x,y,c) e exp]

                  Detach, 964, 970

 

            972  z e n & (x,y,z) e exp

                  E Spec, 971

 

            973  z e n

                  Split, 972

 

            974  (x,y,z) e exp

                  Split, 972

 

            975  ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]

                  U Spec, 943

 

            976  ALL(b):[(x,y) e n2 & b e n => [exp(x,y)=b <=> (x,y,b) e exp]]

                  U Spec, 975

 

            977  (x,y) e n2 & z e n => [exp(x,y)=z <=> (x,y,z) e exp]

                  U Spec, 976

 

            978  (x,y) e n2 & z e n

                  Join, 970, 973

 

            979  exp(x,y)=z <=> (x,y,z) e exp

                  Detach, 977, 978

 

            980  [exp(x,y)=z => (x,y,z) e exp]

             & [(x,y,z) e exp => exp(x,y)=z]

                  Iff-And, 979

 

            981  exp(x,y)=z => (x,y,z) e exp

                  Split, 980

 

            982  (x,y,z) e exp => exp(x,y)=z

                  Split, 980

 

            983  exp(x,y)=z

                  Detach, 982, 974

 

            984  exp(x,y) e n

                  Substitute, 983, 973

 

    As Required:

 

      985  ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

            4 Conclusion, 960

 

        

         Prove: ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

        

         Suppose..

 

            986  x e n

                  Premise

 

            

             Prove: ~x=0 => exp(x,0)=1

            

             Suppose...

 

                  987  ~x=0

                        Premise

 

                  988  x e n => [~x=0 => (x,0,1) e exp]

                        U Spec, 114

 

                  989  ~x=0 => (x,0,1) e exp

                        Detach, 988, 986

 

                  990  (x,0,1) e exp

                        Detach, 989, 987

 

                  991  ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]

                        U Spec, 943

 

                  992  ALL(b):[(x,0) e n2 & b e n => [exp(x,0)=b <=> (x,0,b) e exp]]

                        U Spec, 991

 

                  993  (x,0) e n2 & 1 e n => [exp(x,0)=1 <=> (x,0,1) e exp]

                        U Spec, 992

 

                  994  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                        U Spec, 22

 

                  995  (x,0) e n2 <=> x e n & 0 e n

                        U Spec, 994

 

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

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

                        Iff-And, 995

 

                  997  (x,0) e n2 => x e n & 0 e n

                        Split, 996

 

                  998  x e n & 0 e n => (x,0) e n2

                        Split, 996

 

                  999  x e n & 0 e n

                        Join, 986, 2

 

                  1000 (x,0) e n2

                        Detach, 998, 999

 

                  1001 (x,0) e n2 & 1 e n

                        Join, 1000, 3

 

                  1002 exp(x,0)=1 <=> (x,0,1) e exp

                        Detach, 993, 1001

 

                  1003 [exp(x,0)=1 => (x,0,1) e exp]

                 & [(x,0,1) e exp => exp(x,0)=1]

                        Iff-And, 1002

 

                  1004 exp(x,0)=1 => (x,0,1) e exp

                        Split, 1003

 

                  1005 (x,0,1) e exp => exp(x,0)=1

                        Split, 1003

 

                  1006 exp(x,0)=1

                        Detach, 1005, 990

 

         As Required:

 

            1007 ~x=0 => exp(x,0)=1

                  4 Conclusion, 987

 

    As Required:

 

      1008 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

            4 Conclusion, 986

 

        

         Prove: ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

        

         Suppose...

 

            1009 x e n & y e n

                  Premise

 

            1010 x e n

                  Split, 1009

 

            1011 y e n

                  Split, 1009

 

            1012 ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e exp]]

                  U Spec, 451

 

            1013 (x,y) e n2 => EXIST(c):[c e n & (x,y,c) e exp]

                  U Spec, 1012

 

            1014 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            1015 (x,y) e n2 <=> x e n & y e n

                  U Spec, 1014

 

            1016 [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 1015

 

            1017 (x,y) e n2 => x e n & y e n

                  Split, 1016

 

            1018 x e n & y e n => (x,y) e n2

                  Split, 1016

 

            1019 (x,y) e n2

                  Detach, 1018, 1009

 

            1020 EXIST(c):[c e n & (x,y,c) e exp]

                  Detach, 1013, 1019

 

            1021 z e n & (x,y,z) e exp

                  E Spec, 1020

 

            1022 z e n

                  Split, 1021

 

            1023 (x,y,z) e exp

                  Split, 1021

 

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

             => [(x,b,c) e exp => (x,b+1,c*x) e exp]]

                  U Spec, 168

 

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

             => [(x,y,c) e exp => (x,y+1,c*x) e exp]]

                  U Spec, 1024

 

            1026 x e n & y e n & z e n

             => [(x,y,z) e exp => (x,y+1,z*x) e exp]

                  U Spec, 1025

 

            1027 x e n & y e n & z e n

                  Join, 1009, 1022

 

            1028 (x,y,z) e exp => (x,y+1,z*x) e exp

                  Detach, 1026, 1027

 

            1029 (x,y+1,z*x) e exp

                  Detach, 1028, 1023

 

            1030 ALL(b):[y e n & b e n => y+b e n]

                  U Spec, 6

 

            1031 y e n & 1 e n => y+1 e n

                  U Spec, 1030

 

            1032 y e n & 1 e n

                  Join, 1011, 3

 

            1033 y+1 e n

                  Detach, 1031, 1032

 

            1034 ALL(b):[z e n & b e n => z*b e n]

                  U Spec, 10

 

            1035 z e n & x e n => z*x e n

                  U Spec, 1034

 

            1036 z e n & x e n

                  Join, 1022, 1010

 

            1037 z*x e n

                  Detach, 1035, 1036

 

            1038 ALL(a2):ALL(b):[(x,a2) e n2 & b e n => [exp(x,a2)=b <=> (x,a2,b) e exp]]

                  U Spec, 943

 

            1039 ALL(b):[(x,y) e n2 & b e n => [exp(x,y)=b <=> (x,y,b) e exp]]

                  U Spec, 1038

 

            1040 (x,y) e n2 & z e n => [exp(x,y)=z <=> (x,y,z) e exp]

                  U Spec, 1039

 

            1041 (x,y) e n2 & z e n

                  Join, 1019, 1022

 

            1042 exp(x,y)=z <=> (x,y,z) e exp

                  Detach, 1040, 1041

 

            1043 [exp(x,y)=z => (x,y,z) e exp]

             & [(x,y,z) e exp => exp(x,y)=z]

                  Iff-And, 1042

 

            1044 exp(x,y)=z => (x,y,z) e exp

                  Split, 1043

 

            1045 (x,y,z) e exp => exp(x,y)=z

                  Split, 1043

 

            1046 exp(x,y)=z

                  Detach, 1045, 1023

 

            1047 ALL(b):[(x,y+1) e n2 & b e n => [exp(x,y+1)=b <=> (x,y+1,b) e exp]]

                  U Spec, 1038, 1033

 

            1048 (x,y+1) e n2 & z*x e n => [exp(x,y+1)=z*x <=> (x,y+1,z*x) e exp]

                  U Spec, 1047, 1037

 

            1049 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 22

 

            1050 (x,y+1) e n2 <=> x e n & y+1 e n

                  U Spec, 1049, 1033

 

            1051 [(x,y+1) e n2 => x e n & y+1 e n]

             & [x e n & y+1 e n => (x,y+1) e n2]

                  Iff-And, 1050

 

            1052 (x,y+1) e n2 => x e n & y+1 e n

                  Split, 1051

 

            1053 x e n & y+1 e n => (x,y+1) e n2

                  Split, 1051

 

            1054 x e n & y+1 e n

                  Join, 1010, 1033

 

            1055 (x,y+1) e n2

                  Detach, 1053, 1054

 

            1056 (x,y+1) e n2 & z*x e n

                  Join, 1055, 1037

 

            1057 exp(x,y+1)=z*x <=> (x,y+1,z*x) e exp

                  Detach, 1048, 1056

 

            1058 [exp(x,y+1)=z*x => (x,y+1,z*x) e exp]

             & [(x,y+1,z*x) e exp => exp(x,y+1)=z*x]

                  Iff-And, 1057

 

            1059 exp(x,y+1)=z*x => (x,y+1,z*x) e exp

                  Split, 1058

 

            1060 (x,y+1,z*x) e exp => exp(x,y+1)=z*x

                  Split, 1058

 

            1061 exp(x,y+1)=z*x

                  Detach, 1060, 1029

 

            1062 exp(x,y+1)=exp(x,y)*x

                  Substitute, 1046, 1061

 

    As Required:

 

      1063 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            4 Conclusion, 1009

 

      1064 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

            Join, 985, 959

 

      1065 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

            Join, 1064, 1008

 

      1066 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            Join, 1065, 1063

 

 

As Required:

 

1067 ALL(x0):[x0 e n

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

    & exp(0,0)=x0

    & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

    & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

      4 Conclusion, 14