theorem Th1: :: SCPQSORT:1

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for J being shiftable Program of
for a, b being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b