theorem Th12: :: SCPISORT:12

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
IExec ((for-down (a,i,n,I)),P,s) = IExec ((for-down (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))