theorem Th16: :: SCPINVAR:16

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