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