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