-- ASSOCPROOF

Derivation of:

Nat(Z)
==> X+(Y+Z) = (X+Y)+Z

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

All X Y:
(Nat(!Z)
 ==> X+(Y+!Z) = (X+Y)+!Z)

Applying the axioms

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

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

All X Y:
(Nat(!Z)
 ==> X+Y = (X+Y)+0
       & !Z = 0
     | Any y0:
       (X+suc(Y+y0) = (X+Y)+suc(y0)
        & !Z = suc(y0)))

Simplifying the entire disjunction leads to

All X Y:
(Nat(!Z)
 ==> !Z = 0
     | Any y0:
       (X+suc(Y+y0) = (X+Y)+suc(y0)
        & !Z = suc(y0)))

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

All X Y:
(Nat(!Z)
 ==> !Z = 0
     | Any y0:
       (suc(X+(Y+y0)) = (X+Y)+suc(y0)
        & !Z = suc(y0)))

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

All X Y:
(Nat(!Z)
 ==> !Z = 0
     | Any y0:
       (suc(X+(Y+y0)) = suc((X+Y)+y0)
        & !Z = suc(y0)))

Simplifying the entire disjunction leads to

All X Y:
(Nat(!Z)
 ==> !Z = 0
     | Any y0:
       (X+(Y+y0) = (X+Y)+y0
        & !Z = suc(y0)))

Applying the Horn theorem

X0+(Y0+Z0) = (X0+Y0)+Z0
<=== Nat(Z0)
     & !Z >> Z0

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

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

Applying the axiom

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

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

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

Applying the Horn theorem

suc(x) > x

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

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

Simplifying the entire disjunction leads to

Nat(!Z)
==> !Z = 0
    | Any y0:
      (Nat(y0)
       & !Z = 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

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

Simplifying the entire disjunction leads to

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

Simplifying the entire disjunction leads to

True