theorem Th16: :: SCMPDS_6:25

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