theorem :: SCMISORT:6

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_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )