-- EXPPROOF

Derivation of:

Nat(X)
==> X < 2**X

Selecting induction variables at position [] of summand no. 0 leads to

Nat(!X)
==> !X < 2**!X

Applying the axioms

x**0 = 1
& x**suc(y) = x*(x**y)

 at position [1, 1] of summand no. 0 leads to

Nat(!X)
==> 0 < 1
      & !X = 0
    | Any y0:
      (suc(y0) < 2*(2**y0)
       & !X = suc(y0))

Simplifying the entire disjunction leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (suc(y0) < 2*(2**y0)
       & !X = suc(y0))

Applying the Horn theorem

2*x = x+x

 at position [1, 1, 0, 0, 1] of summand no. 0 leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (suc(y0) < (2**y0)+(2**y0)
       & !X = suc(y0))

Applying the Horn theorem

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

 at position [1, 1, 0, 0] of summand no. 0 leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (suc(y0) < suc(2**y0)
       & !X = suc(y0))

Simplifying the entire disjunction leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (y0 < 2**y0
       & !X = suc(y0))

Applying the Horn theorem

X0 < 2**X0
<=== Nat(X0)
     & !X >> X0

 at position [1, 1, 0, 0] of summand no. 0 leads to

Nat(!X)
==> !X = 0
    | Any y0:
      ((Nat(y0)
          & !X >> y0)
       & !X = suc(y0))

Applying the axiom

(x >> y
 <=== x > y)

 at position [1, 1, 0, 0, 1] of summand no. 0 leads to

Nat(!X)
==> !X = 0
    | Any y0:
      ((Nat(y0)
          & !X > y0)
       & !X = suc(y0))

Simplifying the entire disjunction leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (Nat(y0)
       & !X > y0
       & !X = suc(y0))

Applying the Horn theorem

suc(x) > x

 at position [1, 1, 0, 1] of summand no. 0 leads to

Nat(!X)
==> !X = 0
    | Any y0:
      (Nat(y0)
       & !X = suc(y0)
       & !X = suc(y0))

Applying the co-Horn theorem

Nat(x)
===> x = 0
     | Any y:
       (x = suc(y)
        & Nat(y))

 at position [0] of summand no. 0 leads to

!X = 0
    | Any y:
      (!X = suc(y)
       & Nat(y))
==> !X = 0
    | Any y0:
      (Nat(y0)
       & !X = suc(y0))

Simplifying the entire disjunction leads to

All y:
(!X = suc(y)
     & Nat(y)
 ==> !X = 0
     | Any y0:
       (Nat(y0)
        & !X = suc(y0)))

Simplifying the entire disjunction leads to

True