theorem Th23: :: AMI_8:23

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)) = 4 holds
( ( (Comput (P,s,k)) . (dl. 1) = 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( (Comput (P,s,k)) . (dl. 1) <> 0 implies IC (Comput (P,s,(k + 1))) = 5 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )