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 n, i, p0 being Element of NAT
for f being FinSequence of INT st f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,Q,t)) . c = (p0 + 1) + (len g) & (IExec (I,Q,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,Q,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),P,s)) . b = Sum f & while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )