theorem Th60: :: SCMPDS_2:64

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