Finally we prove the STACK equations.
We show
with the following steps:
  1. Use quantifier elimination to introduce new constants i, n of sort Nat, and a of sort Arr .
  2. Show by reduction that
  3. Introduce the lemma
        ( I, I1, I2: Nat, A : Arr)
                I1 <= I2   implies   I1 || put(I, I2, A) = I1 || A .
  4. Then show by reduction that
        (pop push(n, i || a)) R (i || a) = true .

26 Jun 1997 /html>