(where put(I,I2,A) puts the value I at location I2 in the array A, and where I1 || A indicates the implementation state with pointer I1 and array A.I, I1, I2: Nat,
A : Arr)
I1 <= I2 implies (I1 || put(I, I2, A)) R (I1 || A) .
The applet below illustrates this lemma. The top array and pointer represent a fixed current state, and below that is a copy that we can manipulate. For this, first choose a pointer value by clicking on a position between the two arrays. Next, change the value of a cell above the pointer in the lower array by clicking that cell; a random number will be chosen for its new value. Now, you can try the "pop" and "push" operations to see that the two arrays are indeed "behaviorally" the same.