-- EVODPROOF

Derivation of:

Nat(X)
==> even(X)
    | odd(X)

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

Nat(!X)
==> even(!X)
    | odd(!X)

Applying the axiom(s)

even(0)
& (even(suc(x))
   <=== odd(x))

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

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

Applying the axiom(s)

(odd(suc(x))
 <=== even(x))

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

Nat(!X)
==> (!X = 0
       | Any x0:
         (odd(x0)
          & !X = suc(x0)))
    | Any x1:
      (even(x1)
       & !X = suc(x1))

Simplifying the entire disjunction leads to

Nat(!X)
==> !X = 0
    | Any x0:
      (odd(x0)
       & !X = suc(x0))
    | Any x1:
      (even(x1)
       & !X = suc(x1))

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

Nat(!X)
==> !X = 0
    | Any x1:
      (odd(x1)
       & !X = suc(x1))
    | Any x1:
      (even(x1)
       & !X = suc(x1))

Applying the Horn theorem

even(X0)
     | odd(X0)
<=== Nat(X0)
     & !X >> X0

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

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

Applying the axiom(s)

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

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

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

Simplifying the entire disjunction leads to

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

Applying the Horn theorem

suc(x) > x

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

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

Applying the axiom(s)

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

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

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

Simplifying the entire disjunction leads to

True