theorem Th17: :: AMI_8:17

for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
P halts_at 1