theorem Th3: :: SCMFSA_9:20

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_on s,P & IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0