for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being 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
( if=0 (a,k1,I,J) is_closed_on s,P & if=0 (a,k1,I,J) is_halting_on s,P )