theorem Th18: :: SCMPDS_8:20

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )