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 k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a