theorem Th1: :: SCMISORT:2

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds
for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a