fmod STACK is

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

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

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

*** top of the empty stack
red top(EmptyStack) .

*** pop the empty stack
red pop(EmptyStack) .

*** push A then B on stack, what is
*** on top?
red top(push(push(S,A),B)) .

*** push A then B on stack, then pop
*** stack: what is contents of stack?
red pop(push(push(S,A),B)) .

*** push A then B, then pop stack,
*** what is on top?
red top(pop(push(push(S,A),B))) .