theorem Th2: :: SCPQSORT:2

for P being Instruction-Sequence of SCMPDS
for s, sm being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),m) holds
( DataPart sm = DataPart (IExec (I,P,(Initialize s))) & Initialize sm = sm )