module SIMPLE-NAT {

        [Zero NzNat < Nat]

        op 0 : -> Zero
        op s : Nat -> Nat
        op _+_ : Nat Nat -> Nat

        vars X, Y : Nat
        eq 0 + X = X .
        eq s(X) + Y = s(X + Y) .

    } 

    open SIMPLE-NAT .
    ** op a : -> Nat .
    var a : Nat

    --> Should reduce to 0
    red 0 + 0 .

    --> Inductive hypothesis
    eq a + 0 = a .

    --> Conclusion - should reduce to s(a)
    red s(a) + 0 .
    close