for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a