th STACK is sort Stack .
  pr DATA .
  op empty : -> Stack .
  op push : Nat Stack -> Stack .
  op top_ : Stack -> Nat .
  op pop_ : Stack -> Stack .
  var S : Stack . var I : Nat .
  eq top push(I,S) = I .
  eq pop empty = empty .
  eq pop push(I,S) = S .
endth