theorem Th29: :: SCMPDS_7:31

for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a