theorem :: SCMISORT:7

for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0