theorem Th42: :: SCMPDS_7:44

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