theorem :: SCMPDS_8: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 X being set
for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & f . (Initialize (IExec (I,Q,t))) < f . t & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )