fmod ORDER-STACK is
    sorts Stack NeStack Elt .

    subsort NeStack < Stack .

    op top : NeStack -> Elt .
    op push : Stack Elt -> NeStack .
    op pop : NeStack -> Stack .

    var E : Elt .
    var F : Elt . *** Only used in reductions
    var S : Stack .
    var NeS : NeStack .

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

*** push E on S then take top - should be E
red top(push(S,E)) .

*** push E on S then take top - should be S
red pop(push(S,E)) .

*** push F then E on S then pop it,
*** then take top - should be F
red top(pop(push(push(S,F),E))) .