for s being State of SCM+FSA
for f being FinSeq-Location
for m, n being Nat
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))