theorem Th101: :: SCMPDS_6:110

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