theorem Th18: :: SCMPDS_6:27

for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for s being 0 -started State of SCMPDS
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))