theorem :: SCMPDS_6:104

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being halt-free parahalting shiftable Program of
for a, b being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds
(IExec ((if<0 (a,k1,I,J)),P,(Initialize s))) . b = (IExec (J,P,(Initialize s))) . b