theorem Th27: :: AMI_8:27

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