theorem Th28: :: SCMPDS_5:41

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 parahalting Program of
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a