theorem Th24: :: SCMPDS_6:33

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 Program of st I is_closed_on s,P & I is_halting_on s,P holds
IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))