THEOREM

*******

 

Recall that there are infinitely many exponent-like functions ^ on the natural numbers such that:

 

   1. x^2 = x*x

   2. x^(y+1) = x^y * x

 

See proof

 

Here, we will show that these infinitely many functions will differ ONLY in the value assigned to 0^0, i.e. they will

yield the SAME result for x^y if we do NOT have x = y = 0.

 

 

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

 

 

OUTLINE

*******

 

Lines    Content

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

 

1-7      Axioms/Definition

 

8        Previous result (link to proof)

 

9-13     Define exponent-like functions exp1 and exp2 that start by defining powers of 2

 

14-30    Convert exp1 and exp2 to equivalent functions that start by defining powers of 0

 

31-194   Prove by induction that if ~[x=0 & y=0] then exp1(x,y)=exp2(x,y)

 

 

 

AXIOMS/DEFINITIONS

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

 

Define: n, 0, 1, 2

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

 

Properties of +

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

 

Closed on n

 

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

      Axiom

 

Principle of mathematical deduction using addition on n

 

5     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

 

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

      Axiom

 

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

      Axiom

 

 

PREVIOUS RESULT

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

 

In the context of exponent-like functions, starting by defining powers of 2 is equivalent to starting

by defining powers of 0                                                                                     Proof

 

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

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

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

    <=> ALL(a):[a e n => exp(a,2)=a*a]]]]

      Axiom

 

   

    PROOF

    *****

   

    Suppose...

 

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

         & ALL(a):[a e n => exp1(a,2)=a*a]

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

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

         & ALL(a):[a e n => exp2(a,2)=a*a]

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

            Premise

 

    Define: exp1

 

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

            Split, 9

 

      11   ALL(a):[a e n => exp1(a,2)=a*a]

            Split, 9

 

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

            Split, 9

 

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

         & ALL(a):[a e n => exp2(a,2)=a*a]

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

            Split, 9

 

    Define: exp2

 

      14   ALL(a):ALL(b):[a e n & b e n => exp2(a,b) e n]

            Split, 13

 

      15   ALL(a):[a e n => exp2(a,2)=a*a]

            Split, 13

 

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

            Split, 13

 

    Apply previous result for exp1

 

      17   ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

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

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

         <=> ALL(a):[a e n => exp1(a,2)=a*a]]]

            U Spec, 8

 

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

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

         <=> ALL(a):[a e n => exp1(a,2)=a*a]]

            Detach, 17, 10

 

      19   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

         <=> ALL(a):[a e n => exp1(a,2)=a*a]

            Detach, 18, 12

 

      20   [ALL(a):[a e n => [~a=0 => exp1(a,0)=1]] => ALL(a):[a e n => exp1(a,2)=a*a]]

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

            Iff-And, 19

 

      21   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]] => ALL(a):[a e n => exp1(a,2)=a*a]

            Split, 20

 

      22   ALL(a):[a e n => exp1(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

            Split, 20

 

      23   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

            Detach, 22, 11

 

    Apply previous result for exp2

 

      24   ALL(a):ALL(b):[a e n & b e n => exp2(a,b) e n]

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

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

         <=> ALL(a):[a e n => exp2(a,2)=a*a]]]

            U Spec, 8

 

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

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

         <=> ALL(a):[a e n => exp2(a,2)=a*a]]

            Detach, 24, 14

 

      26   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

         <=> ALL(a):[a e n => exp2(a,2)=a*a]

            Detach, 25, 16

 

      27   [ALL(a):[a e n => [~a=0 => exp2(a,0)=1]] => ALL(a):[a e n => exp2(a,2)=a*a]]

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

            Iff-And, 26

 

      28   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]] => ALL(a):[a e n => exp2(a,2)=a*a]

            Split, 27

 

      29   ALL(a):[a e n => exp2(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

            Split, 27

 

      30   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

            Detach, 29, 15

 

        

         Prove: ALL(a):[a e n

                => ALL(b):[b e n => [~[a=0 & b=0] => exp1(a,b)=exp2(a,b)]]]  (by induction)

        

         Suppose...

 

            31   x e n

                  Premise

 

         Construct set p for proof by induction

 

            32   EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]]

                  Subset, 1

 

            33   Set(p) & ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

                  E Spec, 32

 

         Define: p

 

            34   Set(p)

                  Split, 33

 

            35   ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

                  Split, 33

 

         Apply principle of induction

 

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

 

            

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

            

             Suppose...

 

                  37   y e p

                        Premise

 

                  38   y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        U Spec, 35

 

                  39   [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

                        Iff-And, 38

 

                  40   y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Split, 39

 

                  41   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

                        Split, 39

 

                  42   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Detach, 40, 37

 

                  43   y e n

                        Split, 42

 

         As Required:

 

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

                  4 Conclusion, 37

 

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

                  Join, 34, 44

 

        

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

 

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

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

                  Detach, 36, 45

 

        

         BASE CASE

         *********

        

         Apply definition p

 

            47   0 e p <=> 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

                  U Spec, 35

 

            48   [0 e p => 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]]

             & [0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)] => 0 e p]

                  Iff-And, 47

 

            49   0 e p => 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

                  Split, 48

 

         Sufficient: For 0 e p

 

            50   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)] => 0 e p

                  Split, 48

 

         Two cases to consider:

 

            51   x=0 | ~x=0

                  Or Not

 

             Case 1

            

             Prove: x=0 => 0 e p

            

             Suppose...

 

                  52   x=0

                        Premise

 

                  53   0=0

                        Reflex

 

                  54   x=0 & 0=0

                        Join, 52, 53

 

                

                 Prove: ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

                

                 Suppose...

 

                        55   ~[x=0 & 0=0]

                              Premise

 

                        56   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

                              Arb Cons, 54

 

                        57   exp1(x,0)=exp2(x,0)

                              Detach, 56, 55

 

             As Required:

 

                  58   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

                        4 Conclusion, 55

 

                  59   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

                        Join, 2, 58

 

                  60   0 e p

                        Detach, 50, 59

 

         Case 1

        

         As Required:

 

            61   x=0 => 0 e p

                  4 Conclusion, 52

 

             Case 2

            

             Prove: ~x=0 => 0 e p

            

             Suppose...

 

                  62   ~x=0

                        Premise

 

                

                 Prove: ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

                

                 Suppose...

 

                        63   ~[x=0 & 0=0]

                              Premise

 

                        64   x e n => [~x=0 => exp1(x,0)=1]

                              U Spec, 23

 

                        65   ~x=0 => exp1(x,0)=1

                              Detach, 64, 31

 

                        66   exp1(x,0)=1

                              Detach, 65, 62

 

                        67   x e n => [~x=0 => exp2(x,0)=1]

                              U Spec, 30

 

                        68   ~x=0 => exp2(x,0)=1

                              Detach, 67, 31

 

                        69   exp2(x,0)=1

                              Detach, 68, 62

 

                        70   exp1(x,0)=exp2(x,0)

                              Substitute, 69, 66

 

             As Required:

 

                  71   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

                        4 Conclusion, 63

 

                  72   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

                        Join, 2, 71

 

                  73   0 e p

                        Detach, 50, 72

 

         Case 2

        

         As Required:

 

            74   ~x=0 => 0 e p

                  4 Conclusion, 62

 

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

                  Join, 61, 74

 

         As Required:

 

            76   0 e p

                  Cases, 51, 75

 

            

             INDUCTIVE STEP

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

            

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

            

             Suppose...

 

                  77   y e p

                        Premise

 

             Apply definition of p

 

                  78   y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        U Spec, 35

 

                  79   [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

                        Iff-And, 78

 

                  80   y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Split, 79

 

                  81   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

                        Split, 79

 

                  82   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Detach, 80, 77

 

                  83   y e n

                        Split, 82

 

                  84   ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

                        Split, 82

 

             Apply axiom

 

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

                        U Spec, 4

 

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

                        U Spec, 85

 

                  87   y e n & 1 e n

                        Join, 83, 3

 

                  88   y+1 e n

                        Detach, 86, 87

 

             Apply definition of p

 

                  89   y+1 e p <=> y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]

                        U Spec, 35, 88

 

                  90   [y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]]

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

                        Iff-And, 89

 

                  91   y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]

                        Split, 90

 

            

             Sufficient: For y+1 e p

 

                  92   y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

                        Split, 90

 

                  93   y+1 e n & [~~[x=0 & y+1=0] | exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

                        Imply-Or, 92

 

                  94   y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

                        Rem DNeg, 93

 

                 Case 1

                

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

                

                 Suppose...

 

                        95   x=0

                              Premise

 

                 Two sub-cases to consider:

 

                        96   y=0 | ~y=0

                              Or Not

 

                      Sub-case 1

                     

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

                     

                      Suppose...

 

                              97   y=0

                                    Premise

 

                      Apply definition of exp1

 

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

                                    U Spec, 12

 

                              99   0 e n & 0 e n => exp1(0,0+1)=exp1(0,0)*0

                                    U Spec, 98

 

                              100  0 e n & 0 e n

                                    Join, 2, 2

 

                              101  exp1(0,0+1)=exp1(0,0)*0

                                    Detach, 99, 100

 

                      Apply definition of exp1

 

                              102  ALL(b):[0 e n & b e n => exp1(0,b) e n]

                                    U Spec, 10

 

                              103  0 e n & 0 e n => exp1(0,0) e n

                                    U Spec, 102

 

                              104  0 e n & 0 e n

                                    Join, 2, 2

 

                              105  exp1(0,0) e n

                                    Detach, 103, 104

 

                      Apply axiom

 

                              106  exp1(0,0) e n => exp1(0,0)*0=0

                                    U Spec, 7, 105

 

                              107  exp1(0,0)*0=0

                                    Detach, 106, 105

 

                              108  exp1(0,0+1)=0

                                    Substitute, 107, 101

 

                      Apply definition of exp2

 

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

                                    U Spec, 16

 

                              110  0 e n & 0 e n => exp2(0,0+1)=exp2(0,0)*0

                                    U Spec, 109

 

                              111  exp2(0,0+1)=exp2(0,0)*0

                                    Detach, 110, 104

 

                      Apply definition of exp2

 

                              112  ALL(b):[0 e n & b e n => exp2(0,b) e n]

                                    U Spec, 14

 

                              113  0 e n & 0 e n => exp2(0,0) e n

                                    U Spec, 112

 

                              114  exp2(0,0) e n

                                    Detach, 113, 104

 

                      Apply axiom

 

                              115  exp2(0,0) e n => exp2(0,0)*0=0

                                    U Spec, 7, 114

 

                              116  exp2(0,0)*0=0

                                    Detach, 115, 114

 

                              117  exp2(0,0+1)=0

                                    Substitute, 116, 111

 

                              118  exp1(0,0+1)=exp2(0,0+1)

                                    Substitute, 117, 108

 

                              119  exp1(x,0+1)=exp2(x,0+1)

                                    Substitute, 95, 118

 

                              120  exp1(x,y+1)=exp2(x,y+1)

                                    Substitute, 97, 119

 

                              121  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

                                    Arb Or, 120

 

                              122  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

                                    Join, 88, 121

 

                              123  y+1 e p

                                    Detach, 94, 122

 

                 Sub-case 1

                

                 As Required:

 

                        124  y=0 => y+1 e p

                              4 Conclusion, 97

 

                      Sub-case 2

                     

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

                     

                      Suppose...

 

                              125  ~y=0

                                    Premise

 

                         

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

                         

                          Suppose to the contrary...

 

                                    126  x=0 & y=0

                                          Premise

 

                                    127  x=0

                                          Split, 126

 

                                    128  y=0

                                          Split, 126

 

                                    129  y=0 & ~y=0

                                          Join, 128, 125

 

                      As Required:

 

                              130  ~[x=0 & y=0]

                                    4 Conclusion, 126

 

                              131  exp1(x,y)=exp2(x,y)

                                    Detach, 84, 130

 

                      Apply definition of exp1

 

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

                                    U Spec, 12

 

                              133  x e n & y e n => exp1(x,y+1)=exp1(x,y)*x

                                    U Spec, 132

 

                              134  x e n & y e n

                                    Join, 31, 83

 

                              135  exp1(x,y+1)=exp1(x,y)*x

                                    Detach, 133, 134

 

                      Apply definition of exp2

 

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

                                    U Spec, 16

 

                              137  x e n & y e n => exp2(x,y+1)=exp2(x,y)*x

                                    U Spec, 136

 

                              138  exp2(x,y+1)=exp2(x,y)*x

                                    Detach, 137, 134

 

                              139  exp2(x,y+1)=exp1(x,y)*x

                                    Substitute, 131, 138

 

                              140  exp1(x,y+1)=exp2(x,y+1)

                                    Substitute, 139, 135

 

                              141  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

                                    Arb Or, 140

 

                              142  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

                                    Join, 88, 141

 

                              143  y+1 e p

                                    Detach, 94, 142

 

                 Sub-case 2

                

                 As Required:

 

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

                              4 Conclusion, 125

 

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

                              Join, 124, 144

 

                        146  y+1 e p

                              Cases, 96, 145

 

             Case 1

            

             As Required:

 

                  147  x=0 => y+1 e p

                        4 Conclusion, 95

 

                 Case 2

                

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

                

                 Suppose...

 

                        148  ~x=0

                              Premise

 

                     

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

                     

                      Suppose to the contrary...

 

                              149  x=0 & y=0

                                    Premise

 

                              150  x=0

                                    Split, 149

 

                              151  y=0

                                    Split, 149

 

                              152  x=0 & ~x=0

                                    Join, 150, 148

 

                 As Required:

 

                        153  ~[x=0 & y=0]

                              4 Conclusion, 149

 

                        154  exp1(x,y)=exp2(x,y)

                              Detach, 84, 153

 

                 Apply definition of exp1

 

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

                              U Spec, 12

 

                        156  x e n & y e n => exp1(x,y+1)=exp1(x,y)*x

                              U Spec, 155

 

                        157  x e n & y e n

                              Join, 31, 83

 

                        158  exp1(x,y+1)=exp1(x,y)*x

                              Detach, 156, 157

 

                 Apply definition of exp2

 

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

                              U Spec, 16

 

                        160  x e n & y e n => exp2(x,y+1)=exp2(x,y)*x

                              U Spec, 159

 

                        161  x e n & y e n

                              Join, 31, 83

 

                        162  exp2(x,y+1)=exp2(x,y)*x

                              Detach, 160, 161

 

                        163  exp2(x,y+1)=exp1(x,y)*x

                              Substitute, 154, 162

 

                        164  exp1(x,y+1)=exp2(x,y+1)

                              Substitute, 163, 158

 

                        165  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

                              Arb Or, 164

 

                        166  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

                              Join, 88, 165

 

                        167  y+1 e p

                              Detach, 94, 166

 

             Case 2

            

             As Required:

 

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

                        4 Conclusion, 148

 

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

                        Join, 147, 168

 

                  170  y+1 e p

                        Cases, 51, 169

 

         As Required:

 

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

                  4 Conclusion, 77

 

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

                  Join, 76, 171

 

         As Required:

 

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

                  Detach, 46, 172

 

            

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

            

             Suppose...

 

                  174  y e n

                        Premise

 

                  175  y e n => y e p

                        U Spec, 173

 

                  176  y e p

                        Detach, 175, 174

 

             Apply definition of p

 

                  177  y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        U Spec, 35

 

                  178  [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

                 & [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

                        Iff-And, 177

 

                  179  y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Split, 178

 

                  180  y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

                        Split, 178

 

                  181  y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                        Detach, 179, 176

 

                  182  y e n

                        Split, 181

 

                  183  ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

                        Split, 181

 

         As Required:

 

            184  ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

                  4 Conclusion, 174

 

    As Required:

 

      185  ALL(a):[a e n

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

            4 Conclusion, 31

 

        

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

        

         Suppose...

 

            186  x e n & y e n

                  Premise

 

            187  x e n

                  Split, 186

 

            188  y e n

                  Split, 186

 

            189  x e n

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

                  U Spec, 185

 

            190  ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

                  Detach, 189, 187

 

            191  y e n => [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

                  U Spec, 190

 

            192  ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

                  Detach, 191, 188

 

    As Required:

 

      193  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp1(a,b)=exp2(a,b)]]

            4 Conclusion, 186

 

 

As Required:

 

194  ALL(exp1):ALL(exp2):[ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

    & ALL(a):[a e n => exp1(a,2)=a*a]

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

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

    & ALL(a):[a e n => exp2(a,2)=a*a]

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

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

      4 Conclusion, 9