We prove the key lemma that
(
I, I1, I2: Nat,
A : Arr)
I1 <= I2
implies
(I1 || put(I, I2, A)) R (I1 || A)
.
We use
induction
on
NAT
, with the signature
{0,s}
.
Induction requires that we do the following:
base case:
prove the assertion for
0
.
induction step:
prove the assertion for
s n
, assuming it for
n
.
21 December 1996