theorem Th62: :: SCMPDS_6:71

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of
for J being halt-free shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds
IExec ((if>0 (a,k1,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))