SUBSTITUTION IN PROGRAMS WITH ARRAYS

The Pre condition is

{ (if 3=i then 4 else a(3)) =2 and
(if i = i then 4 else a(i)) = 4}

or

{i != 3 and a(3) =2}

The above Pre condition can be simplified:

{i != 3 and a(3) =2}
a(i) := 4;
{a(3)=2 and a(i)=4}