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>