theorem Th2: :: SCMFSA_9:19

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
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )