theorem :: SCPISORT:13

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 being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) > 0 & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . a = s . a holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )