theorem Th24: :: AMI_8:24

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