THEOREM

*******

 

There exists a unique exponent function on n with 0^0 left undefined.

 

Existence of exp(a,b):

 

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

   & exp(0,1)=0

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

   & ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]

 

Uniqueness of exp(a,b):

 

   ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

   & exp(0,1)=0

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

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

   => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

 

   & [ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

   & exp'(0,1)=0

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

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

   => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]

 

   => ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

 

 

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-10-17

 

 

AXIOMS/DEFINITIONS

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

 

Define: n, 0, 1

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

4     ~1=0

      Axiom

 

5     0+1=1

      Axiom

 

 

Properties of +

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

 

Closed on n

 

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

      Axiom

 

Adding 0

 

7     ALL(a):[a e n => a+0=a]

      Axiom

 

+ Commutative

 

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

      Axiom

 

+ Right cancelable

 

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

      Axiom

 

0 is "first" number

 

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

      Axiom

 

Principle of Mathematical Induction

 

11   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

 

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

      Axiom

 

Multiplying by 0

 

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

      Axiom

 

Multiplying by 1

 

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

      Axiom

 

* Commutative

 

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

      Axiom

 

 

Function Axiom (2 varibles)

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

 

16   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

 

PREVIOUS RESULT

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

 

There exists infinitely many exponent-like functions starting with exponent 0    Proof

 

17   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]]]

      Axiom

 

   

    PROOF

*****

 

Suppose...

 

      18   x0 e n

            Premise

 

    Apply previous result

 

      19   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]]

            U Spec, 17

 

      20   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]]

            Detach, 19, 18

 

      21   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]

            E Spec, 20

 

   

    Define: exp

    ***********

 

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

            Split, 21

 

      23   exp(0,0)=x0

            Split, 21

 

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

            Split, 21

 

      25   ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            Split, 21

 

   

    Construct n2

 

      26   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

 

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

 

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

            U Spec, 27

 

      29   Set(n) & Set(n)

            Join, 1, 1

 

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

            Detach, 28, 29

 

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

            E Spec, 30

 

   

    Define: n2

 

      32   Set'(n2)

            Split, 31

 

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

            Split, 31

 

   

    Construct n3

 

      34   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

 

      35   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, 34

 

      36   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, 35

 

      37   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, 36

 

      38   Set(n) & Set(n)

            Join, 1, 1

 

      39   Set(n) & Set(n) & Set(n)

            Join, 38, 1

 

      40   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, 37, 39

 

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

            E Spec, 40

 

   

    Define: n3

 

      42   Set''(n3)

            Split, 41

 

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

            Split, 41

 

   

    Construct dom

 

      44   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]

            Subset, 32

 

      45   Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]

            E Spec, 44

 

   

    Define: dom

 

      46   Set'(dom)

            Split, 45

 

      47   ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]

            Split, 45

 

   

    Construct exp'

 

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

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

            Subset, 42

 

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

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

            E Spec, 48

 

   

    Define: exp'

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

 

      50   Set''(exp')

            Split, 49

 

      51   ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'

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

            Split, 49

 

   

    Apply Function Axioms (for 2 variables)

 

      52   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

 

      53   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, 52

 

      54   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, 53

 

      55   Set''(exp') & Set'(dom) & Set(n)

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

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

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & 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 dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]

            U Spec, 54

 

      56   Set''(exp') & Set'(dom)

            Join, 50, 46

 

      57   Set''(exp') & Set'(dom) & Set(n)

            Join, 56, 1

 

   

    Sufficient: For functionality of exp'

 

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

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

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & 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 dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]

            Detach, 55, 57

 

        

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

        

         Suppose...

 

            59   (x,y,z) e exp'

                  Premise

 

         Apply definition of exp'

 

            60   ALL(b):ALL(c):[(x,b,c) e exp'

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

                  U Spec, 51

 

            61   ALL(c):[(x,y,c) e exp'

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

                  U Spec, 60

 

            62   (x,y,z) e exp'

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

                  U Spec, 61

 

            63   [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]

             & [(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']

                  Iff-And, 62

 

            64   (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                  Split, 63

 

            65   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'

                  Split, 63

 

            66   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                  Detach, 64, 59

 

            67   (x,y,z) e n3

                  Split, 66

 

            68   ~[x=0 & y=0] & z=exp(x,y)

                  Split, 66

 

            69   ~[x=0 & y=0]

                  Split, 68

 

            70   z=exp(x,y)

                  Split, 68

 

            71   ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                  U Spec, 47

 

            72   (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                  U Spec, 71

 

            73   [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

             & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                  Iff-And, 72

 

            74   (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                  Split, 73

 

         Apply definition of n3

 

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

                  U Spec, 43

 

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

                  U Spec, 75

 

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

                  U Spec, 76

 

            78   [(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, 77

 

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

                  Split, 78

 

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

                  Split, 78

 

            81   x e n & y e n & z e n

                  Detach, 79, 67

 

            82   x e n

                  Split, 81

 

            83   y e n

                  Split, 81

 

            84   z e n

                  Split, 81

 

         Sufficient: For (x,y) e dom

 

            85   (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                  Split, 73

 

         Apply definition of n3

 

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

                  U Spec, 43

 

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

                  U Spec, 86

 

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

                  U Spec, 87

 

            89   [(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, 88

 

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

                  Split, 89

 

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

                  Split, 89

 

            92   x e n & y e n & z e n

                  Detach, 90, 67

 

            93   x e n

                  Split, 92

 

            94   y e n

                  Split, 92

 

            95   z e n

                  Split, 92

 

         Apply definition of n2

 

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

                  U Spec, 33

 

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

                  U Spec, 96

 

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

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

                  Iff-And, 97

 

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

                  Split, 98

 

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

                  Split, 98

 

            101  x e n & y e n

                  Join, 82, 83

 

            102  (x,y) e n2

                  Detach, 100, 101

 

            103  (x,y) e n2 & ~[x=0 & y=0]

                  Join, 102, 69

 

            104  (x,y) e dom

                  Detach, 85, 103

 

            105  (x,y) e dom & z e n

                  Join, 104, 84

 

    Functionality of exp', Part 1

 

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

            4 Conclusion, 59

 

        

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

        

         Suppose...

 

            107  (x,y) e dom

                  Premise

 

         Apply definition of dom

 

            108  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                  U Spec, 47

 

            109  (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                  U Spec, 108

 

            110  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

             & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                  Iff-And, 109

 

            111  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                  Split, 110

 

            112  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                  Split, 110

 

            113  (x,y) e n2 & ~[x=0 & y=0]

                  Detach, 111, 107

 

            114  (x,y) e n2

                  Split, 113

 

            115  ~[x=0 & y=0]

                  Split, 113

 

         Apply definition of exp'

 

            116  ALL(b):ALL(c):[(x,b,c) e exp'

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

                  U Spec, 51

 

            117  ALL(c):[(x,y,c) e exp'

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

                  U Spec, 116

 

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

                  U Spec, 22

 

            119  x e n & y e n => exp(x,y) e n

                  U Spec, 118

 

         Apply definition of n2

 

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

                  U Spec, 33

 

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

                  U Spec, 120

 

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

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

                  Iff-And, 121

 

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

                  Split, 122

 

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

                  Split, 122

 

            125  x e n & y e n

                  Detach, 123, 114

 

            126  x e n

                  Split, 125

 

            127  y e n

                  Split, 125

 

            128  exp(x,y) e n

                  Detach, 119, 125

 

            129  (x,y,exp(x,y)) e exp'

             <=> (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  U Spec, 117, 128

 

            130  [(x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]]

             & [(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp']

                  Iff-And, 129

 

            131  (x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  Split, 130

 

         Sufficient: For (x,y,exp(x,y)) e exp'

 

            132  (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp'

                  Split, 130

 

         Apply definition of n3

 

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

                  U Spec, 43

 

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

                  U Spec, 133

 

            135  (x,y,exp(x,y)) e n3 <=> x e n & y e n & exp(x,y) e n

                  U Spec, 134, 128

 

            136  [(x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n]

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

                  Iff-And, 135

 

            137  (x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n

                  Split, 136

 

         Sufficient: For (x,y,exp(x,y)) e n3

 

            138  x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3

                  Split, 136

 

            139  x e n & y e n & exp(x,y) e n

                  Join, 125, 128

 

            140  (x,y,exp(x,y)) e n3

                  Detach, 138, 139

 

            141  exp(x,y)=exp(x,y)

                  Reflex, 128

 

            142  ~[x=0 & y=0] & exp(x,y)=exp(x,y)

                  Join, 115, 141

 

            143  (x,y,exp(x,y)) e n3

             & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  Join, 140, 142

 

            144  (x,y,exp(x,y)) e exp'

                  Detach, 132, 143

 

            145  exp(x,y) e n & (x,y,exp(x,y)) e exp'

                  Join, 128, 144

 

            146  EXIST(b):[b e n & (x,y,b) e exp']

                  E Gen, 145

 

    Functionality of exp', Part 2

 

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

            4 Conclusion, 107

 

        

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

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

        

         Suppose...

 

            148  (x,y) e dom & z1 e n & z2 e n

                  Premise

 

            149  (x,y) e dom

                  Split, 148

 

            150  z1 e n

                  Split, 148

 

            151  z2 e n

                  Split, 148

 

            

             Suppose...

 

                  152  (x,y,z1) e exp' & (x,y,z2) e exp'

                        Premise

 

                  153  (x,y,z1) e exp'

                        Split, 152

 

                  154  (x,y,z2) e exp'

                        Split, 152

 

             Apply the definition of exp'

 

                  155  ALL(b):ALL(c):[(x,b,c) e exp'

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

                        U Spec, 51

 

                  156  ALL(c):[(x,y,c) e exp'

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

                        U Spec, 155

 

                  157  (x,y,z1) e exp'

                 <=> (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        U Spec, 156

 

                  158  [(x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]]

                 & [(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp']

                        Iff-And, 157

 

                  159  (x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        Split, 158

 

                  160  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp'

                        Split, 158

 

                  161  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        Detach, 159, 153

 

                  162  (x,y,z1) e n3

                        Split, 161

 

                  163  ~[x=0 & y=0] & z1=exp(x,y)

                        Split, 161

 

                  164  ~[x=0 & y=0]

                        Split, 163

 

                  165  z1=exp(x,y)

                        Split, 163

 

                  166  (x,y,z2) e exp'

                 <=> (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        U Spec, 156

 

                  167  [(x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]]

                 & [(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp']

                        Iff-And, 166

 

                  168  (x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        Split, 167

 

                  169  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp'

                        Split, 167

 

                  170  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        Detach, 168, 154

 

                  171  (x,y,z2) e n3

                        Split, 170

 

                  172  ~[x=0 & y=0] & z2=exp(x,y)

                        Split, 170

 

                  173  ~[x=0 & y=0]

                        Split, 172

 

                  174  z2=exp(x,y)

                        Split, 172

 

                  175  z1=z2

                        Substitute, 174, 165

 

            176  (x,y,z1) e exp' & (x,y,z2) e exp' => z1=z2

                  4 Conclusion, 152

 

    Functionality of exp', Part 3

 

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

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

            4 Conclusion, 148

 

    Joining results...

 

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

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

            Join, 106, 147

 

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

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

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

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

            Join, 178, 177

 

   

    exp' is a partial binary function on n

   

    As Required:

 

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

            Detach, 58, 179

 

        

         Prove: ALL(x):ALL(y):[x e n & y e n => [~[x=0 & y=0] => exp'(x,y) e n]]

        

         Suppose...

 

            181  x e n & y e n

                  Premise

 

            

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

            

             Suppose...

 

                  182  ~[x=0 & y=0]

                        Premise

 

             Apply definition of exp'

 

                  183  ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]

                        U Spec, 147

 

                  184  (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']

                        U Spec, 183

 

             Apply definition of dom

 

                  185  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  186  (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                        U Spec, 185

 

                  187  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

                 & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                        Iff-And, 186

 

                  188  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                        Split, 187

 

                  189  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                        Split, 187

 

             Apply definition of n2

 

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

                        U Spec, 33

 

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

                        U Spec, 190

 

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

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

                        Iff-And, 191

 

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

                        Split, 192

 

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

                        Split, 192

 

                  195  (x,y) e n2

                        Detach, 194, 181

 

                  196  (x,y) e n2 & ~[x=0 & y=0]

                        Join, 195, 182

 

                  197  (x,y) e dom

                        Detach, 189, 196

 

                  198  EXIST(b):[b e n & (x,y,b) e exp']

                        Detach, 184, 197

 

                  199  z e n & (x,y,z) e exp'

                        E Spec, 198

 

                  200  z e n

                        Split, 199

 

                  201  (x,y,z) e exp'

                        Split, 199

 

             Apply previous result

 

                  202  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  203  ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]

                        U Spec, 202

 

                  204  (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']

                        U Spec, 203

 

                  205  (x,y) e dom & z e n

                        Join, 197, 200

 

                  206  exp'(x,y)=z <=> (x,y,z) e exp'

                        Detach, 204, 205

 

                  207  [exp'(x,y)=z => (x,y,z) e exp']

                 & [(x,y,z) e exp' => exp'(x,y)=z]

                        Iff-And, 206

 

                  208  exp'(x,y)=z => (x,y,z) e exp'

                        Split, 207

 

                  209  (x,y,z) e exp' => exp'(x,y)=z

                        Split, 207

 

                  210  exp'(x,y)=z

                        Detach, 209, 201

 

                  211  exp'(x,y) e n

                        Substitute, 210, 200

 

         As Required:

 

            212  ~[x=0 & y=0] => exp'(x,y) e n

                  4 Conclusion, 182

 

   

    As Required:

 

      213  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

            4 Conclusion, 181

 

   

    Prove: exp'(0,1)=0

   

    Apply definition of exp'

 

      214  ALL(b):ALL(c):[(0,b,c) e exp'

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

            U Spec, 51

 

      215  ALL(c):[(0,1,c) e exp'

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

            U Spec, 214

 

      216  (0,1,0) e exp'

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

            U Spec, 215

 

      217  [(0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]]

         & [(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp']

            Iff-And, 216

 

      218  (0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

            Split, 217

 

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

 

      219  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp'

            Split, 217

 

    Apply definition of n3

 

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

            U Spec, 43

 

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

            U Spec, 220

 

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

            U Spec, 221

 

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

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

            Iff-And, 222

 

      224  (0,1,0) e n3 => 0 e n & 1 e n & 0 e n

            Split, 223

 

      225  0 e n & 1 e n & 0 e n => (0,1,0) e n3

            Split, 223

 

      226  0 e n & 1 e n

            Join, 2, 3

 

      227  0 e n & 1 e n & 0 e n

            Join, 226, 2

 

      228  (0,1,0) e n3

            Detach, 225, 227

 

        

         Prove: ~[0=0 & 1=0]

        

         Suppose to the contrary...

 

            229  0=0 & 1=0

                  Premise

 

            230  0=0

                  Split, 229

 

            231  1=0

                  Split, 229

 

            232  1=0 & ~1=0

                  Join, 231, 4

 

      233  ~[0=0 & 1=0]

            4 Conclusion, 229

 

    Apply definition of exp

 

      234  ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]

            U Spec, 25

 

      235  0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0

            U Spec, 234

 

      236  0 e n & 0 e n

            Join, 2, 2

 

      237  exp(0,0+1)=exp(0,0)*0

            Detach, 235, 236

 

      238  ALL(b):[0 e n & b e n => 0+b=b+0]

            U Spec, 8

 

      239  0 e n & 1 e n => 0+1=1+0

            U Spec, 238

 

      240  0 e n & 1 e n

            Join, 2, 3

 

      241  0+1=1+0

            Detach, 239, 240

 

      242  1 e n => 1+0=1

            U Spec, 7

 

      243  1+0=1

            Detach, 242, 3

 

      244  0+1=1

            Substitute, 243, 241

 

      245  exp(0,1)=exp(0,0)*0

            Substitute, 244, 237

 

      246  ALL(b):[0 e n & b e n => exp(0,b) e n]

            U Spec, 22

 

      247  0 e n & 0 e n => exp(0,0) e n

            U Spec, 246

 

      248  0 e n & 0 e n

            Join, 2, 2

 

      249  exp(0,0) e n

            Detach, 247, 248

 

      250  exp(0,0) e n => exp(0,0)*0=0

            U Spec, 13, 249

 

      251  exp(0,0)*0=0

            Detach, 250, 249

 

      252  exp(0,1)=0

            Substitute, 251, 245

 

      253  0=exp(0,1)

            Sym, 252

 

      254  ~[0=0 & 1=0] & 0=exp(0,1)

            Join, 233, 253

 

      255  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

            Join, 228, 254

 

      256  (0,1,0) e exp'

            Detach, 219, 255

 

    Apply previous result

 

      257  ALL(a2):ALL(b):[(0,a2) e dom & b e n => [exp'(0,a2)=b <=> (0,a2,b) e exp']]

            U Spec, 180

 

      258  ALL(b):[(0,1) e dom & b e n => [exp'(0,1)=b <=> (0,1,b) e exp']]

            U Spec, 257

 

      259  (0,1) e dom & 0 e n => [exp'(0,1)=0 <=> (0,1,0) e exp']

            U Spec, 258

 

    Apply defintion of dom

 

      260  ALL(b):[(0,b) e dom <=> (0,b) e n2 & ~[0=0 & b=0]]

            U Spec, 47

 

      261  (0,1) e dom <=> (0,1) e n2 & ~[0=0 & 1=0]

            U Spec, 260

 

      262  [(0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]]

         & [(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom]

            Iff-And, 261

 

      263  (0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]

            Split, 262

 

      264  (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom

            Split, 262

 

      265  ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]

            U Spec, 33

 

      266  (0,1) e n2 <=> 0 e n & 1 e n

            U Spec, 265

 

      267  [(0,1) e n2 => 0 e n & 1 e n]

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

            Iff-And, 266

 

      268  (0,1) e n2 => 0 e n & 1 e n

            Split, 267

 

      269  0 e n & 1 e n => (0,1) e n2

            Split, 267

 

      270  0 e n & 1 e n

            Join, 2, 3

 

      271  (0,1) e n2

            Detach, 269, 270

 

            272  0=0 & 1=0

                  Premise

 

            273  0=0

                  Split, 272

 

            274  1=0

                  Split, 272

 

            275  1=0 & ~1=0

                  Join, 274, 4

 

      276  ~[0=0 & 1=0]

            4 Conclusion, 272

 

      277  (0,1) e n2 & ~[0=0 & 1=0]

            Join, 271, 276

 

      278  (0,1) e dom

            Detach, 264, 277

 

      279  (0,1) e dom & 0 e n

            Join, 278, 2

 

      280  exp'(0,1)=0 <=> (0,1,0) e exp'

            Detach, 259, 279

 

      281  [exp'(0,1)=0 => (0,1,0) e exp']

         & [(0,1,0) e exp' => exp'(0,1)=0]

            Iff-And, 280

 

      282  exp'(0,1)=0 => (0,1,0) e exp'

            Split, 281

 

      283  (0,1,0) e exp' => exp'(0,1)=0

            Split, 281

 

   

    As Required:

 

      284  exp'(0,1)=0

            Detach, 283, 256

 

        

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

        

         Suppose...

 

            285  x e n

                  Premise

 

            

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

            

             Suppose...

 

                  286  ~x=0

                        Premise

 

                  287  ALL(b):ALL(c):[(x,b,c) e exp'

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

                        U Spec, 51

 

                  288  ALL(c):[(x,0,c) e exp'

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

                        U Spec, 287

 

                  289  (x,0,1) e exp'

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

                        U Spec, 288

 

                  290  [(x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]]

                 & [(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp']

                        Iff-And, 289

 

                  291  (x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

                        Split, 290

 

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

 

                  292  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp'

                        Split, 290

 

             Apply definition of n3

 

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

                        U Spec, 43

 

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

                        U Spec, 293

 

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

                        U Spec, 294

 

                  296  [(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, 295

 

                  297  [(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, 295

 

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

                        Split, 297

 

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

                        Split, 297

 

                  300  x e n & 0 e n

                        Join, 285, 2

 

                  301  x e n & 0 e n & 1 e n

                        Join, 300, 3

 

                  302  (x,0,1) e n3

                        Detach, 299, 301

 

                        303  x=0 & 0=0

                              Premise

 

                        304  x=0

                              Split, 303

 

                        305  0=0

                              Split, 303

 

                        306  x=0 & ~x=0

                              Join, 304, 286

 

                  307  ~[x=0 & 0=0]

                        4 Conclusion, 303

 

             Apply definition of exp

 

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

                        U Spec, 24

 

                  309  ~x=0 => exp(x,0)=1

                        Detach, 308, 285

 

                  310  exp(x,0)=1

                        Detach, 309, 286

 

                  311  1=exp(x,0)

                        Sym, 310

 

                  312  ~[x=0 & 0=0] & 1=exp(x,0)

                        Join, 307, 311

 

                  313  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

                        Join, 302, 312

 

                  314  (x,0,1) e exp'

                        Detach, 292, 313

 

                  315  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  316  ALL(b):[(x,0) e dom & b e n => [exp'(x,0)=b <=> (x,0,b) e exp']]

                        U Spec, 315

 

                  317  (x,0) e dom & 1 e n => [exp'(x,0)=1 <=> (x,0,1) e exp']

                        U Spec, 316

 

             Apply definition of dom

 

                  318  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  319  (x,0) e dom <=> (x,0) e n2 & ~[x=0 & 0=0]

                        U Spec, 318

 

                  320  [(x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]]

                 & [(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom]

                        Iff-And, 319

 

                  321  (x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]

                        Split, 320

 

                  322  (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom

                        Split, 320

 

             Apply definition of n2

 

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

                        U Spec, 33

 

                  324  (x,0) e n2 <=> x e n & 0 e n

                        U Spec, 323

 

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

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

                        Iff-And, 324

 

                  326  (x,0) e n2 => x e n & 0 e n

                        Split, 325

 

                  327  x e n & 0 e n => (x,0) e n2

                        Split, 325

 

                  328  x e n & 0 e n

                        Join, 285, 2

 

                  329  (x,0) e n2

                        Detach, 327, 328

 

                        330  x=0 & 0=0

                              Premise

 

                        331  x=0

                              Split, 330

 

                        332  0=0

                              Split, 330

 

                        333  x=0 & ~x=0

                              Join, 331, 286

 

                  334  ~[x=0 & 0=0]

                        4 Conclusion, 330

 

                  335  (x,0) e n2 & ~[x=0 & 0=0]

                        Join, 329, 334

 

                  336  (x,0) e dom

                        Detach, 322, 335

 

                  337  (x,0) e dom & 1 e n

                        Join, 336, 3

 

                  338  exp'(x,0)=1 <=> (x,0,1) e exp'

                        Detach, 317, 337

 

                  339  [exp'(x,0)=1 => (x,0,1) e exp']

                 & [(x,0,1) e exp' => exp'(x,0)=1]

                        Iff-And, 338

 

                  340  exp'(x,0)=1 => (x,0,1) e exp'

                        Split, 339

 

                  341  (x,0,1) e exp' => exp'(x,0)=1

                        Split, 339

 

                  342  exp'(x,0)=1

                        Detach, 341, 314

 

         As Required:

 

            343  ~x=0 => exp'(x,0)=1

                  4 Conclusion, 286

 

   

    As Required:

 

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

            4 Conclusion, 285

 

        

         Prove: ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]

        

        Suppose...

 

            345  x e n & y e n

                  Premise

 

            346  x e n

                  Split, 345

 

            347  y e n

                  Split, 345

 

            

             Prove: ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x

            

             Suppose...

 

                  348  ~[x=0 & y=0]

                        Premise

 

             Apply previous result

 

                  349  ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]

                        U Spec, 147

 

                  350  (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']

                        U Spec, 349

 

             Apply definition of dom

 

                  351  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  352  (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                        U Spec, 351

 

                  353  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

                 & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                        Iff-And, 352

 

                  354  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                        Split, 353

 

                  355  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                        Split, 353

 

             Apply definition of n2

 

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

                        U Spec, 33

 

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

                        U Spec, 356

 

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

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

                        Iff-And, 357

 

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

                        Split, 358

 

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

                        Split, 358

 

                  361  (x,y) e n2

                        Detach, 360, 345

 

                  362  (x,y) e n2 & ~[x=0 & y=0]

                        Join, 361, 348

 

                  363  (x,y) e dom

                        Detach, 355, 362

 

                  364  EXIST(b):[b e n & (x,y,b) e exp']

                        Detach, 350, 363

 

                  365  z e n & (x,y,z) e exp'

                        E Spec, 364

 

                  366  z e n

                        Split, 365

 

                  367  (x,y,z) e exp'

                        Split, 365

 

                  368  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  369  ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]

                        U Spec, 368

 

                  370  (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']

                        U Spec, 369

 

                  371  ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]

                        U Spec, 368

 

                  372  (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']

                        U Spec, 371

 

                  373  (x,y) e dom & z e n

                        Join, 363, 366

 

                  374  exp'(x,y)=z <=> (x,y,z) e exp'

                        Detach, 372, 373

 

                  375  [exp'(x,y)=z => (x,y,z) e exp']

                 & [(x,y,z) e exp' => exp'(x,y)=z]

                        Iff-And, 374

 

                  376  exp'(x,y)=z => (x,y,z) e exp'

                        Split, 375

 

                  377  (x,y,z) e exp' => exp'(x,y)=z

                        Split, 375

 

                  378  exp'(x,y)=z

                        Detach, 377, 367

 

                  379  ALL(b):ALL(c):[(x,b,c) e exp'

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

                        U Spec, 51

 

                  380  ALL(c):[(x,y,c) e exp'

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

                        U Spec, 379

 

                  381  (x,y,z) e exp'

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

                        U Spec, 380

 

                  382  [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]

                 & [(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']

                        Iff-And, 381

 

                  383  (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                        Split, 382

 

                  384  (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'

                        Split, 382

 

                  385  (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                        Detach, 383, 367

 

                  386  (x,y,z) e n3

                        Split, 385

 

                  387  ~[x=0 & y=0] & z=exp(x,y)

                        Split, 385

 

                  388  ~[x=0 & y=0]

                        Split, 387

 

                  389  z=exp(x,y)

                        Split, 387

 

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

                        U Spec, 6

 

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

                        U Spec, 390

 

                  392  y e n & 1 e n

                        Join, 347, 3

 

                  393  y+1 e n

                        Detach, 391, 392

 

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

                        U Spec, 12

 

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

                        U Spec, 394

 

                  396  z e n & x e n

                        Join, 366, 346

 

                  397  z*x e n

                        Detach, 395, 396

 

             Apply definition of exp'

 

                  398  ALL(b):ALL(c):[(x,b,c) e exp'

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

                        U Spec, 51

 

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

                 <=> (x,y+1,c) e n3 & [~[x=0 & y+1=0] & c=exp(x,y+1)]]

                        U Spec, 398, 393

 

                  400  (x,y+1,z*x) e exp'

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

                        U Spec, 399, 397

 

                  401  [(x,y+1,z*x) e exp' => (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]]

                 & [(x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)] => (x,y+1,z*x) e exp']

                        Iff-And, 400

 

                  402  (x,y+1,z*x) e exp' => (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]

                        Split, 401

 

                  403  (x,y+1,z*x) e n3 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)] => (x,y+1,z*x) e exp'

                        Split, 401

 

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

                        U Spec, 43

 

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

                        U Spec, 404, 393

 

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

                        U Spec, 405, 397

 

                  407  [(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, 406

 

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

                        Split, 407

 

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

                        Split, 407

 

                  410  x e n & y+1 e n

                        Join, 346, 393

 

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

                        Join, 410, 397

 

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

                        Detach, 409, 411

 

                

                  Prove: ~[x=0 & y+1=0]

                

                 Suppose to the contrary...

 

                        413  x=0 & y+1=0

                              Premise

 

                        414  x=0

                              Split, 413

 

                        415  y+1=0

                              Split, 413

 

                        416  y e n => ~y+1=0

                              U Spec, 10

 

                        417  ~y+1=0

                              Detach, 416, 347

 

                        418  y+1=0 & ~y+1=0

                              Join, 415, 417

 

             As Required:

 

                  419  ~[x=0 & y+1=0]

                        4 Conclusion, 413

 

                  420  ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]

                        U Spec, 25

 

                  421  x e n & y e n => exp(x,y+1)=exp(x,y)*x

                        U Spec, 420

 

                  422  exp(x,y+1)=exp(x,y)*x

                        Detach, 421, 345

 

                  423  exp(x,y+1)=z*x

                        Substitute, 389, 422

 

                  424  z*x=exp(x,y+1)

                        Sym, 423

 

                  425  ~[x=0 & y+1=0] & z*x=exp(x,y+1)

                        Join, 419, 424

 

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

                 & [~[x=0 & y+1=0] & z*x=exp(x,y+1)]

                        Join, 412, 425

 

                  427  (x,y+1,z*x) e exp'

                        Detach, 403, 426

 

                  428  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  429  ALL(b):[(x,y+1) e dom & b e n => [exp'(x,y+1)=b <=> (x,y+1,b) e exp']]

                        U Spec, 428, 393

 

                  430  (x,y+1) e dom & z*x e n => [exp'(x,y+1)=z*x <=> (x,y+1,z*x) e exp']

                        U Spec, 429, 397

 

                  431  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  432  (x,y+1) e dom <=> (x,y+1) e n2 & ~[x=0 & y+1=0]

                        U Spec, 431, 393

 

                  433  [(x,y+1) e dom => (x,y+1) e n2 & ~[x=0 & y+1=0]]

                 & [(x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e dom]

                        Iff-And, 432

 

                  434  (x,y+1) e dom => (x,y+1) e n2 & ~[x=0 & y+1=0]

                        Split, 433

 

                  435  (x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e dom

                        Split, 433

 

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

                        U Spec, 33

 

                  437  (x,y+1) e n2 <=> x e n & y+1 e n

                        U Spec, 436, 393

 

                  438  [(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, 437

 

                  439  (x,y+1) e n2 => x e n & y+1 e n

                        Split, 438

 

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

                        Split, 438

 

                  441  x e n & y+1 e n

                        Join, 346, 393

 

                  442  (x,y+1) e n2

                        Detach, 440, 441

 

                  443  (x,y+1) e n2 & ~[x=0 & y+1=0]

                        Join, 442, 419

 

                  444  (x,y+1) e dom

                        Detach, 435, 443

 

                  445  (x,y+1) e dom & z*x e n

                        Join, 444, 397

 

                  446  exp'(x,y+1)=z*x <=> (x,y+1,z*x) e exp'

                        Detach, 430, 445

 

                  447  [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, 446

 

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

                        Split, 447

 

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

                        Split, 447

 

                  450  exp'(x,y+1)=z*x

                        Detach, 449, 427

 

                  451  exp'(x,y+1)=exp'(x,y)*x

                        Substitute, 378, 450

 

         As Required:

 

            452  ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x

                  4 Conclusion, 348

 

   

    As Required:

 

      453  ALL(a):ALL(b):[a e n & b e n

         => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]

            4 Conclusion, 345

 

      454  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

         & exp'(0,1)=0

            Join, 213, 284

 

      455  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

         & exp'(0,1)=0

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

            Join, 454, 344

 

      456  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

         & exp'(0,1)=0

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

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

         => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]

            Join, 455, 453

 

As Required:

 

457  ALL(x0):[x0 e n

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

    & exp(0,1)=0

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

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

    => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]]

      4 Conclusion, 18

 

458  0 e n

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

    & exp(0,1)=0

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

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

    => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]

      U Spec, 457

 

As Required:

 

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

    & exp(0,1)=0

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

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

    => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]

      Detach, 458, 2

 

   

    Prove the exp function is unique

   

    Suppose...

 

      460  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

         & exp(0,1)=0

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

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

         => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

         & [ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

         & exp'(0,1)=0

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

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

         => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]

            Premise

 

   

    Define: exp

 

      461  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

            Split, 460

 

      462  exp(0,1)=0

            Split, 460

 

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

            Split, 460

 

      464  ALL(a):ALL(b):[a e n & b e n

         => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

            Split, 460

 

      465  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

         & exp'(0,1)=0

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

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

         => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]

            Split, 460

 

   

    Define: exp'

 

      466  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

            Split, 465

 

      467  exp'(0,1)=0

            Split, 465

 

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

            Split, 465

 

      469  ALL(a):ALL(b):[a e n & b e n

         => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]

            Split, 465

 

        

         Prove: ALL(a):[a e n

                => ALL(b):[b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

        

         Suppose...

 

            470  x e n

                  Premise

 

         Two cases to consider:

 

            471  x=0 | ~x=0

                  Or Not

 

         Construct subset p of n

        

         Apply Subset Axiom

 

            472  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]]

                  Subset, 1

 

            473  Set(p) & ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

                  E Spec, 472

 

        

         Define: p

 

            474  Set(p)

                  Split, 473

 

            475  ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

                  Split, 473

 

        

         Apply Principle of Mathematical Induction

 

            476  Set(p) & ALL(b):[b e p => b e n]

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

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

                  U Spec, 11

 

            

             Prove p is a subset of n

            

             Suppose...

 

                  477  y e p

                        Premise

 

             Apply definition of p

 

                  478  y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        U Spec, 475

 

                  479  [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]

                        Iff-And, 478

 

                  480  y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Split, 479

 

                  481  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p

                        Split, 479

 

                  482  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Detach, 480, 477

 

                  483  y e n

                        Split, 482

 

         As Required:

 

            484  ALL(b):[b e p => b e n]

                  4 Conclusion, 477

 

            485  Set(p) & ALL(b):[b e p => b e n]

                  Join, 474, 484

 

        

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

 

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

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

                  Detach, 476, 485

 

        

         Base Case

         *********

        

         Apply definiton of p

 

            487  0 e p <=> 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]

                  U Spec, 475

 

            488  [0 e p => 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]]

             & [0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)] => 0 e p]

                  Iff-And, 487

 

            489  0 e p => 0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)]

                  Split, 488

 

        

         Sufficient: For 0 e p

 

            490  0 e n & [~[x=0 & 0=0] => exp(x,0)=exp'(x,0)] => 0 e p

                  Split, 488

 

            491  0 e n & [~~[x=0 & 0=0] | exp(x,0)=exp'(x,0)] => 0 e p

                  Imply-Or, 490

 

            492  0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)] => 0 e p

                  Rem DNeg, 491

 

             Case 1

            

             Prove: x=0 => 0 e p

            

             Suppose...

 

                  493  x=0

                        Premise

 

                  494  0=0

                        Reflex

 

                  495  x=0 & 0=0

                        Join, 493, 494

 

                  496  x=0 & 0=0 | exp(x,0)=exp'(x,0)

                        Arb Or, 495

 

                  497  0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)]

                        Join, 2, 496

 

                  498  0 e p

                        Detach, 492, 497

 

         Case 1

        

         As Required:

 

            499  x=0 => 0 e p

                  4 Conclusion, 493

 

            

             Case 2

            

             Prove: ~x=0 => 0 e p

            

             Suppose...

 

                  500  ~x=0

                        Premise

 

             Apply definition of exp

 

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

                        U Spec, 463

 

                  502  ~x=0 => exp(x,0)=1

                        Detach, 501, 470

 

                  503  exp(x,0)=1

                        Detach, 502, 500

 

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

                        U Spec, 468

 

                  505  ~x=0 => exp'(x,0)=1

                        Detach, 504, 470

 

                  506  exp'(x,0)=1

                        Detach, 505, 500

 

                  507  exp(x,0)=exp'(x,0)

                        Substitute, 506, 503

 

                  508  x=0 & 0=0 | exp(x,0)=exp'(x,0)

                        Arb Or, 507

 

                  509  0 e n & [x=0 & 0=0 | exp(x,0)=exp'(x,0)]

                        Join, 2, 508

 

                  510  0 e p

                        Detach, 492, 509

 

         Case 2

        

         As Required:

 

            511  ~x=0 => 0 e p

                  4 Conclusion, 500

 

            512  [x=0 => 0 e p] & [~x=0 => 0 e p]

                  Join, 499, 511

 

        

         Apply Cases Rule

        

         As Required:

 

            513  0 e p

                  Cases, 471, 512

 

            

             Inductive Step

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

            

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

            

             Suppose...

 

                  514  y e p

                        Premise

 

             Two sub-cases to consider:

 

                  515  y=0 | ~y=0

                        Or Not

 

             Apply definition of p

 

                  516  y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        U Spec, 475

 

                  517  [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]

                        Iff-And, 516

 

                  518  y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Split, 517

 

                  519  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p

                        Split, 517

 

                  520  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Detach, 518, 514

 

                  521  y e n

                        Split, 520

 

                  522  ~[x=0 & y=0] => exp(x,y)=exp'(x,y)

                        Split, 520

 

                  523  ~~[x=0 & y=0] | exp(x,y)=exp'(x,y)

                        Imply-Or, 522

 

                  524  x=0 & y=0 | exp(x,y)=exp'(x,y)

                        Rem DNeg, 523

 

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

                        U Spec, 6

 

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

                        U Spec, 525

 

                  527  y e n & 1 e n

                        Join, 521, 3

 

                  528  y+1 e n

                        Detach, 526, 527

 

             Apply definition of p

 

                  529  y+1 e p <=> y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]

                        U Spec, 475, 528

 

                  530  [y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]]

                 & [y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)] => y+1 e p]

                        Iff-And, 529

 

                  531  y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)]

                        Split, 530

 

            

             Sufficient: For y+1 e p

 

                  532  y+1 e n & [~[x=0 & y+1=0] => exp(x,y+1)=exp'(x,y+1)] => y+1 e p

                        Split, 530

 

                  533  y+1 e n & [~~[x=0 & y+1=0] | exp(x,y+1)=exp'(x,y+1)] => y+1 e p

                        Imply-Or, 532

 

                  534  y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)] => y+1 e p

                        Rem DNeg, 533

 

                 Case 1

                

                 Prove: x=0 => y+1 e p

                

                 Suppose...

 

                        535  x=0

                              Premise

 

                      Sub-case 1

                     

                      Prove: y=0 => y+1 e p

                     

                      Suppose...

 

                              536  y=0

                                    Premise

 

                              537  y+1 e n & [0=0 & y+1=0 | exp(0,y+1)=exp'(0,y+1)] => y+1 e p

                                    Substitute, 535, 534

 

                              538  y+1 e n & [0=0 & 0+1=0 | exp(0,0+1)=exp'(0,0+1)] => y+1 e p

                                    Substitute, 536, 537

 

                              539  y+1 e n & [0=0 & 1=0 | exp(0,1)=exp'(0,1)] => y+1 e p

                                    Substitute, 5, 538

 

                              540  exp(0,1)=exp'(0,1)

                                    Substitute, 467, 462

 

                              541  0=0 & 1=0 | exp(0,1)=exp'(0,1)

                                    Arb Or, 540

 

                              542  y+1 e n & [0=0 & 1=0 | exp(0,1)=exp'(0,1)]

                                    Join, 528, 541

 

                              543  y+1 e p

                                    Detach, 539, 542

 

                 Sub-case 1

                

                 As Required:

 

                        544  y=0 => y+1 e p

                              4 Conclusion, 536

 

                     

                      Sub-case 2

                     

                      Prove: ~y=0 => y+1 e p

                     

                      Suppose...

 

                              545  ~y=0

                                    Premise

 

                              546  y+1 e n & [0=0 & y+1=0 | exp(0,y+1)=exp'(0,y+1)] => y+1 e p

                                    Substitute, 535, 534

 

                         

                          Prove: ~[x=0 & y=0]

                         

                          Suppose to the contrary...

 

                                    547  x=0 & y=0

                                          Premise

 

                                    548  x=0

                                          Split, 547

 

                                    549  y=0

                                          Split, 547

 

                                    550  y=0 & ~y=0

                                          Join, 549, 545

 

                      As Required:

 

                              551  ~[x=0 & y=0]

                                    4 Conclusion, 547

 

                              552  exp(x,y)=exp'(x,y)

                                    Detach, 522, 551

 

                      Apply definition of exp

 

                              553  ALL(b):[x e n & b e n

                          => [~[x=0 & b=0] => exp(x,b+1)=exp(x,b)*x]]

                                    U Spec, 464

 

                              554  x e n & y e n

                          => [~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x]

                                    U Spec, 553

 

                              555  x e n & y e n

                                    Join, 470, 521

 

                              556  ~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x

                                    Detach, 554, 555

 

                              557  exp(x,y+1)=exp(x,y)*x

                                    Detach, 556, 551

 

                      Apply definition of exp'

 

                              558  ALL(b):[x e n & b e n

                          => [~[x=0 & b=0] => exp'(x,b+1)=exp'(x,b)*x]]

                                    U Spec, 469

 

                              559  x e n & y e n

                          => [~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x]

                                    U Spec, 558

 

                              560  ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x

                                    Detach, 559, 555

 

                              561  exp'(x,y+1)=exp'(x,y)*x

                                    Detach, 560, 551

 

                              562  exp'(x,y+1)=exp(x,y)*x

                                    Substitute, 552, 561

 

                              563  exp(x,y+1)=exp'(x,y+1)

                                    Substitute, 562, 557

 

                              564  x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)

                                    Arb Or, 563

 

                              565  y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)]

                                    Join, 528, 564

 

                              566  y+1 e p

                                    Detach, 534, 565

 

                 Sub-case 2

                

                 As Required:

 

                        567  ~y=0 => y+1 e p

                              4 Conclusion, 545

 

                        568  [y=0 => y+1 e p] & [~y=0 => y+1 e p]

                              Join, 544, 567

 

                        569  y+1 e p

                              Cases, 515, 568

 

             Case 1

            

             As Required:

 

                  570  x=0 => y+1 e p

                        4 Conclusion, 535

 

                 Case 2

                

                 Prove: ~x=0 => y+1 e p

                

                 Suppose...

 

                        571  ~x=0

                              Premise

 

                     

                      Prove: ~[x=0 & y=0]

                     

                      Suppose to the contrary...

 

                              572  x=0 & y=0

                                    Premise

 

                              573  x=0

                                    Split, 572

 

                              574  y=0

                                    Split, 572

 

                              575  x=0 & ~x=0

                                    Join, 573, 571

 

                 As Required:

 

                        576  ~[x=0 & y=0]

                              4 Conclusion, 572

 

                        577  exp(x,y)=exp'(x,y)

                              Detach, 522, 576

 

                 Apply definition of exp

 

                        578  ALL(b):[x e n & b e n

                      => [~[x=0 & b=0] => exp(x,b+1)=exp(x,b)*x]]

                              U Spec, 464

 

                        579  x e n & y e n

                      => [~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x]

                              U Spec, 578

 

                        580  x e n & y e n

                              Join, 470, 521

 

                        581  ~[x=0 & y=0] => exp(x,y+1)=exp(x,y)*x

                              Detach, 579, 580

 

                        582  exp(x,y+1)=exp(x,y)*x

                              Detach, 581, 576

 

                 Apply definition of exp'

 

                        583  ALL(b):[x e n & b e n

                      => [~[x=0 & b=0] => exp'(x,b+1)=exp'(x,b)*x]]

                              U Spec, 469

 

                        584  x e n & y e n

                      => [~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x]

                              U Spec, 583

 

                        585  ~[x=0 & y=0] => exp'(x,y+1)=exp'(x,y)*x

                              Detach, 584, 580

 

                        586  exp'(x,y+1)=exp'(x,y)*x

                              Detach, 585, 576

 

                        587  exp'(x,y+1)=exp(x,y)*x

                              Substitute, 577, 586

 

                        588  exp(x,y+1)=exp'(x,y+1)

                              Substitute, 587, 582

 

                        589  x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)

                              Arb Or, 588

 

                        590  y+1 e n & [x=0 & y+1=0 | exp(x,y+1)=exp'(x,y+1)]

                              Join, 528, 589

 

                        591  y+1 e p

                              Detach, 534, 590

 

             Case 2

            

             As Required:

 

                  592  ~x=0 => y+1 e p

                        4 Conclusion, 571

 

                  593  [x=0 => y+1 e p] & [~x=0 => y+1 e p]

                        Join, 570, 592

 

                  594  y+1 e p

                        Cases, 471, 593

 

         As Required:

 

            595  ALL(b):[b e p => b+1 e p]

                  4 Conclusion, 514

 

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

                  Join, 513, 595

 

            597  ALL(b):[b e n => b e p]

                  Detach, 486, 596

 

            

             Prove: ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

            

             Suppose...

 

                  598  y e n

                        Premise

 

                  599  y e n => y e p

                        U Spec, 597

 

                  600  y e p

                        Detach, 599, 598

 

             Apply definition of p

 

                  601  y e p <=> y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        U Spec, 475

 

                  602  [y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p]

                        Iff-And, 601

 

                  603  y e p => y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Split, 602

 

                  604  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)] => y e p

                        Split, 602

 

                  605  y e n & [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                        Detach, 603, 600

 

                  606  y e n

                        Split, 605

 

                  607  ~[x=0 & y=0] => exp(x,y)=exp'(x,y)

                        Split, 605

 

         As Required:

 

            608  ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

                  4 Conclusion, 598

 

    As Required:

 

      609  ALL(a):[a e n

         => ALL(b):[b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

            4 Conclusion, 470

 

        

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

        

         Suppose...

 

            610  x e n & y e n

                  Premise

 

            611  x e n

                  Split, 610

 

            612  y e n

                  Split, 610

 

            613  x e n

             => ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

                  U Spec, 609

 

            614  ALL(b):[b e n => [~[x=0 & b=0] => exp(x,b)=exp'(x,b)]]

                  Detach, 613, 611

 

            615  y e n => [~[x=0 & y=0] => exp(x,y)=exp'(x,y)]

                  U Spec, 614

 

            616  ~[x=0 & y=0] => exp(x,y)=exp'(x,y)

                  Detach, 615, 612

 

    As Required:

 

      617  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]

            4 Conclusion, 610

 

 

As Required:

 

618  ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

    & exp(0,1)=0

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

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

    => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

    & [ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

    & exp'(0,1)=0

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

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

    => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]

    => ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

      4 Conclusion, 460