for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a