th PTR||ARR is sort Stack .
  pr ARR .
  op _||_ : Nat Arr -> Stack [prec 10].
  op empty : -> Stack .
  op push : Nat Stack -> Stack .
  op top_ : Stack -> Nat .
  op pop_ : Stack -> Stack .
  var I N : Nat . var A : Arr .
  eq empty = 0 || nil . 
  eq push(N, I || A) = s I || put(N,I,A) .
  eq top s I || A = A[I] .
  eq top 0 || A = 0 .
  eq pop s I || A = I || A .
  eq pop 0 || A = 0 || A .
endth