theorem Th7: :: SCPQSORT:7

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )