theorem Th26: :: AMI_8:26

for k being Nat
for i, i1, i2 being Integer
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st I is sequential & I is 0 -dl.constant & IterativeAlgorithm I c= P holds
for s being 0 -started State-consisting of <%i,i1,i2%> holds (Comput (P,s,k)) . (dl. 0) = i