theorem Th25: :: AMI_8:25

for k being Nat
for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st I is sequential & IterativeAlgorithm I c= P & IC (Comput (P,s,0)) = 0 holds
IC (Comput (P,s,k)) in {0,1,2,3,4,5}