theorem :: AMI_5:7

for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM