-- POTPROOF


Derivation of

    Nat(N)
==> (N**2)+N = suc(N)*N

Applying the axioms

  x+0 = x
& x+suc(y) = suc(x+y)

at position [1,0] of the preceding tree leads to the formula

    Nat(N)
==>     0**2 = suc(0)*0
      & N = 0
    | Any y0:
      (  suc((suc(y0)**2)+y0) = suc(suc(y0))*suc(y0)
       & N = suc(y0))

Simplifying (4 steps) the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc((suc(y0)**2)+y0) = suc(suc(y0))*suc(y0)
       & N = suc(y0))

Applying the axiom

x*suc(y) = x+(x*y)

at position [1,1,0,0,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc((suc(y0)**2)+y0) = suc(suc(y0))+(suc(suc(y0))*y0)
       & N = suc(y0))

Reversing the subtrees at positions [1,1,0,0,1,0],[1,1,0,0,1,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc((suc(y0)**2)+y0) = (suc(suc(y0))*y0)+suc(suc(y0))
       & N = suc(y0))

Applying the axiom

x+suc(y) = suc(x+y)

at position [1,1,0,0,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc((suc(y0)**2)+y0) = suc((suc(suc(y0))*y0)+suc(y0))
       & N = suc(y0))

Simplifying the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  (suc(y0)**2)+y0 = (suc(suc(y0))*y0)+suc(y0)
       & N = suc(y0))

Narrowing (3 steps) at position [1,1,0,0] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  (suc(y0)+(suc(y0)*y0))+y0 = suc((suc(suc(y0))*y0)+y0)
       & N = suc(y0))

Reversing the subtrees at positions [1,1,0,0,0,0,0],[1,1,0,0,0,0,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  ((suc(y0)*y0)+suc(y0))+y0 = suc((suc(suc(y0))*y0)+y0)
       & N = suc(y0))

Applying the axiom

x+suc(y) = suc(x+y)

at position [1,1,0,0,0,0] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc((suc(y0)*y0)+y0)+y0 = suc((suc(suc(y0))*y0)+y0)
       & N = suc(y0))

Reversing the subtrees at positions [1,1,0,0,0,0],[1,1,0,0,0,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  y0+suc((suc(y0)*y0)+y0) = suc((suc(suc(y0))*y0)+y0)
       & N = suc(y0))

Applying the axiom

x+suc(y) = suc(x+y)

at position [1,1,0,0,0] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  suc(y0+((suc(y0)*y0)+y0)) = suc((suc(suc(y0))*y0)+y0)
       & N = suc(y0))

Simplifying the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  y0+((suc(y0)*y0)+y0) = (suc(suc(y0))*y0)+y0
       & N = suc(y0))

Reversing the subtrees at positions [1,1,0,0,1,0,0],[1,1,0,0,1,0,1] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  y0+((suc(y0)*y0)+y0) = (y0*suc(suc(y0)))+y0
       & N = suc(y0))

Applying the axiom

x*suc(y) = x+(x*y)

at position [1,1,0,0,1,0] of the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (  y0+((suc(y0)*y0)+y0) = (y0+(y0*suc(y0)))+y0
       & N = suc(y0))

Simplifying (2 steps) the preceding tree leads to the formula

    Nat(N)
==>   N = 0
    | Any y0:
      (N = suc(y0))

Applying the axioms

  Nat(0)
& (     Nat(suc(x))
   <=== Nat(x))

at position [0] of the preceding tree leads to the formula

      N = 0
    | Any x0:
      (  Nat(x0)
       & N = suc(x0))
==>   N = 0
    | Any y0:
      (N = suc(y0))

Simplifying (6 steps) the entire formula leads to True.