:: deftheorem defines IterativeAlgorithm AMI_8:def 4 :
for OPER being Instruction of SCM holds IterativeAlgorithm OPER = <%((dl. 1) >0_goto 2),(halt SCM),OPER,(SubFrom ((dl. 1),(dl. 0))),((dl. 1) =0_goto 1),(SCM-goto 2)%>;