theorem Th18: :: AMI_8:18

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, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k)