theorem Th30: :: AMI_8:30

for k, n being Nat
for i being Integer
for I being Instruction of SCM st ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) holds
for s being 0 -started State-consisting of <%1,n,i%>
for P being IterativeAlgorithm b₄ -extending Instruction-Sequence of SCM holds (Comput (P,s,k)) . (dl. 1) is natural