fmod BASIC-NAT is
        sort Nat .

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

        vars N M : Nat .

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


fmod STACK is
    protecting BASIC-NAT .

    sort Stack .

    op EmptyStack : -> Stack .
    op ErrorElt : -> Nat .
    
    op push : Stack Nat -> Stack .
    op pop : Stack -> Stack .
    op top : Stack -> Nat .
    op isEmpty : Stack -> Bool .
    
    var S : Stack .
    var N : Nat .
    
    *** Just used in the reductions
    vars A B : Nat .

    eq isEmpty(EmptyStack) = true .
    eq isEmpty(push(S,N)) = false .

    eq top(EmptyStack) = ErrorElt .
    eq top(push(S,N)) = N .
    
    eq pop(EmptyStack) = EmptyStack .
    eq pop(push(S,N)) = S .
endfm