fmod BASIC-NAT2 is
        sort Nat .

        op 0 : -> Nat [ctor] .
        op s : Nat -> Nat [ctor iter] .
        op _+_ : Nat Nat -> Nat .

        vars N M : Nat .

        eq 0 + N = N .
        eq s(M) + N = s(M + N) .
endfm

reduce s^5(0) + s^3(0) .