theorem Th6: :: SCPINVAR:6

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, f0, f1 being Int_position
for n, i being Element of NAT st s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 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 & (IExec (I,Q,t)) . f0 = Fib (k + 1) & (IExec (I,Q,t)) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec ((while>0 (a,i,I)),P,s)) . f0 = Fib n & (IExec ((while>0 (a,i,I)),P,s)) . f1 = Fib (n + 1) & while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )