(Commentary in dark blue font. Statements in black, red and green font.)

 

INTRODUCTION

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

 

Here we present formal proof that:

 

1. There exists infinitely many binary functions ^ on the set of natural numbers N such that:

 

     x^2 = x*x

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

 

2. These functions differ ONLY in the value assigned to 0^0.

 

This suggests that exponentiation on N is indeterminate for 0^0.

 

 

THEOREM

*******

 

1.   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 => exp(a,2)=a*a]

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

 

2.   ALL(x1):ALL(x2):[x1 e n & x2 e n

 

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

     & exp(0,0)=x1

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

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

 

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

     & exp'(0,0)=x2

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

     & ALL(a):ALL(b):[a e n & b e n => 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 formal, machine-verified proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

 

 

AXIOMS USED

***********

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

 

Lemma 1  (Proof here)

*******

 

For every x0 e n, there exists a binary function exp on n such that:

 

exp(0,0) = x0

exp(x,1) = 1 for ~x =0

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

 

 

4     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

 

Lemma 2   (Proof here)

*******

 

For every x0 e n, and binary function exp on n we have:

 

exp(0,0) = x0

exp(x,1) = 1 for ~x =0

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

 

if and only if...

 

exp(0,0) = x0

exp(x,2) = x * x

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

 

5     ALL(x0):[x0 e n

    => ALL(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]

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

    & exp(0,0)=x0

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

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

      Axiom

 

 

Lemma 3   (Proof here)

*******

 

For every x1, x2 e n, and binary functions exp and exp’ on n:

 

If

 

exp(0,0) = x1

exp(x,1) = 1 for ~x =0

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

 

and

 

exp’(0,0) = x2

exp’(x,1) = 1 for ~x =0

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

 

then

 

exp(x,y) = exp’(x,y) except for possibly when x = y = 0.

 

6     ALL(x1):ALL(x2):[x1 e n & x2 e n

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

    & exp(0,0)=x1

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

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

    & exp'(0,0)=x2

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

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

      Axiom

 

   

    PROOF

    *****

   

    Prove: 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 => exp(a,2)=a*a]

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

   

    Suppose...

 

      7     x e n

            Premise

 

    Apply Lemma 1

 

      8     x e n

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

         & exp(0,0)=x

         & 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, 4

 

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

         & exp(0,0)=x

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

 

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

         & exp(0,0)=x

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

 

    Apply Lemma 2

 

      11   x e n

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

         & exp(0,0)=x

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

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

         & exp(0,0)=x

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

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

            U Spec, 5

 

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

         & exp(0,0)=x

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

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

         & exp(0,0)=x

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

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

            Detach, 11, 7

 

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

         & exp(0,0)=x

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

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

         & exp(0,0)=x

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

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

            U Spec, 12

 

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

         & exp(0,0)=x

         & 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] => ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x

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

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

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

         & exp(0,0)=x

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

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

         & exp(0,0)=x

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

            Iff-And, 13

 

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

         & exp(0,0)=x

         & 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] => ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x

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

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

            Split, 14

 

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

         & exp(0,0)=x

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

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

         & exp(0,0)=x

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

            Split, 14

 

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

         & exp(0,0)=x

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

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

            Detach, 15, 10

 

As Required:

 

18   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 => exp(a,2)=a*a]

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

      4 Conclusion, 7

 

   

    Prove: ALL(x1):ALL(x2):[x1 e n & x2 e n

   

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

           & exp(0,0)=x1

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

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

   

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

           & exp'(0,0)=x2

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

           & ALL(a):ALL(b):[a e n & b e n => 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)]]]]

   

    Suppose...

 

      19   x1 e n & x2 e n

            Premise

 

      20   x1 e n

            Split, 19

 

      21   x2 e n

            Split, 19

 

        

         Suppose we have binary functions exp and exp' such that..

 

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

             & exp(0,0)=x1

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

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

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

             & exp'(0,0)=x2

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

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

                  Premise

 

         We know from above that such functions exist in n:

        

         Define: exp  (with exp(0,0)=x1)

 

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

                  Split, 22

 

            24   exp(0,0)=x1

                  Split, 22

 

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

                  Split, 22

 

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

                  Split, 22

 

        

         Define: exp'  (with exp'(0,0)=x2)

 

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

                  Split, 22

 

            28   exp'(0,0)=x2

                  Split, 22

 

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

                  Split, 22

 

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

                  Split, 22

 

         Apply Lemma 3

 

            31   ALL(x2):[x1 e n & x2 e n

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  U Spec, 6

 

            32   x1 e n & x2 e n

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  U Spec, 31

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  Detach, 32, 19

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  U Spec, 33

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  U Spec, 34

 

         Apply Lemma 2  (for exp)

 

            36   x1 e n

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

             & exp(0,0)=x1

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

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

             & exp(0,0)=x1

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

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

                  U Spec, 5

 

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

             & exp(0,0)=x1

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

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

             & exp(0,0)=x1

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

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

                  Detach, 36, 20

 

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

             & exp(0,0)=x1

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

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

             & exp(0,0)=x1

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

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

                  U Spec, 37

 

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

             & exp(0,0)=x1

             & 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] => ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

             & exp(0,0)=x1

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

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

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

             & exp(0,0)=x1

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

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

             & exp(0,0)=x1

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

                  Iff-And, 38

 

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

             & exp(0,0)=x1

             & 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] => ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

             & exp(0,0)=x1

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

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

                  Split, 39

 

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

             & exp(0,0)=x1

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

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

             & exp(0,0)=x1

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

                  Split, 39

 

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

             & exp(0,0)=x1

                  Join, 23, 24

 

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

             & exp(0,0)=x1

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

                  Join, 42, 25

 

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

             & exp(0,0)=x1

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

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

                  Join, 43, 26

 

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

             & exp(0,0)=x1

             & 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, 41, 44

 

         Apply Lemma 2  (for exp')

 

            46   x2 e n

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

             & exp(0,0)=x2

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

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

             & exp(0,0)=x2

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

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

                  U Spec, 5

 

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

             & exp(0,0)=x2

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

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

             & exp(0,0)=x2

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

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

                  Detach, 46, 21

 

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

             & exp'(0,0)=x2

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

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

             & exp'(0,0)=x2

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

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

                  U Spec, 47

 

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

             & exp'(0,0)=x2

             & 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] => ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

             & exp'(0,0)=x2

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

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

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

             & exp'(0,0)=x2

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

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

             & exp'(0,0)=x2

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

                  Iff-And, 48

 

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

             & exp'(0,0)=x2

             & 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] => ALL(a):ALL(b):[a e n & b e n => exp'(a,b) e n]

             & exp'(0,0)=x2

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

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

                  Split, 49

 

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

             & exp'(0,0)=x2

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

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

             & exp'(0,0)=x2

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

                  Split, 49

 

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

             & exp'(0,0)=x2

                  Join, 27, 28

 

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

             & exp'(0,0)=x2

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

                  Join, 52, 29

 

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

             & exp'(0,0)=x2

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

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

                  Join, 53, 30

 

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

             & exp'(0,0)=x2

             & 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, 51, 54

 

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

                  Split, 55

 

            57   exp'(0,0)=x2

                  Split, 55

 

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

                  Split, 55

 

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

                  Split, 55

 

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

             & exp(0,0)=x1

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

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

                  Join, 45, 56

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

                  Join, 60, 57

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

                  Join, 61, 58

 

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

             & exp(0,0)=x1

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

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

             & exp'(0,0)=x2

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

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

                  Join, 62, 59

 

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

                  Detach, 35, 63

 

    As Required:

 

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

         & exp(0,0)=x1

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

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

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

         & exp'(0,0)=x2

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

         & ALL(a):ALL(b):[a e n & b e n => 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, 22

 

As Required:

 

66   ALL(x1):ALL(x2):[x1 e n & x2 e n

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

    & exp(0,0)=x1

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

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

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

    & exp'(0,0)=x2

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

    & ALL(a):ALL(b):[a e n & b e n => 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, 19