theorem Th71: :: SCMFSA_2:78

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