theorem :: AMI_3:14

for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = (IC s) + 1 holds
not I is halting by Lm2;