We show that R  is preserved by all operations in .
We show
( I1,I2,N : Nat, A1,A2 : Arr)
        (I1 || A1) R (I2 || A2)
 
implies
                pop(I1 || A1)  R   pop(I2 || A2)   and
                push(N, I1 || A1)  R  push(N, I2 || A2) ,
with the following steps:
  1. Use quantifier elimination, introducing new constants i1, i2 of sort Nat, and a1, a2 of sort Arr.
  2. Use implication elimination, assuming (i1 || a1) R (i2 || a2).
  3. Use case analysis, i1 = 0 or i1 = s(j) for some j of sort Nat.
    3A.  In case i1 = 0 :
    3A1.  Use relation expansion to add i2 = 0 to the hypotheses.
    3A2.  Show by conjunction elimination that
    3A2A.  pop(i1 || a1)  R  pop(i2 || a2) = true
    3A2B.  push(n, i1 || a1)  R   push(n, i2 || a2) = true
    separately by reduction.
    3B.  In case i1 = s(j) :
    3B1.  Use relation expansion to add the following equations to the hypotheses:
    • i2 = s j
    • a2[j] = a1[j]
    • (j || a1) R (j || a2) = true .
    3B2. Show by conjunction elimination separately that
    3B2A. pop(i1 || a1)  R  pop(i2 || a2) = true
    by reduction.
    3B2B. push(n, i1 || a1)  R   push(n, i2 || a2) = true
    3B2B1. by introducing the lemma
    ( I, I1, I2: Nat, A : Arr) I1 <= I2
            implies   I1 || put(I, I2, A) = I1 || A .
    and then by reduction.

18 Jun 1997 dy>