theorem Th16: :: AMI_8:16

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )