let I be Instruction of SCMPDS; :: thesis: ( ex s being State of SCMPDS st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting )
given s being State of SCMPDS such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; :: thesis: not I is halting
assume I is halting ; :: thesis: contradiction
then (Exec (I,s)) . (IC ) = s . NAT by Th6, EXTPRO_1:def 3;
hence contradiction by A1, Th6; :: thesis: verum
IC s = s . NAT by AMI_2:22, FUNCT_7:def 1;
then reconsider w = s . NAT as Element of NAT ;