theorem Th18: :: SCMRING2:18

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