theorem Th20: :: SCMFSA7B:21

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of
for a being Int-Location st not I destroys a holds
for k being Nat holds (Comput ((P +* I),(Initialize s),k)) . a = s . a