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