let I be Instruction of SCM+FSA; :: thesis: ( ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = (IC s) + 1 implies not I is halting )
given s being State of SCM+FSA such that A1: (Exec (I,s)) . (IC ) = (IC s) + 1 ; :: thesis: not I is halting
reconsider T = s as SCM+FSA-State by CARD_3:107;
IC T = T . NAT ;
then reconsider w = T . NAT as Nat ;
assume I is halting ; :: thesis: contradiction
then A2: (Exec (I,s)) . (IC ) = T . NAT by Th1;
(Exec (I,s)) . (IC ) = w + 1 by A1, SCMFSA_1:5, SUBSET_1:def 8;
hence contradiction by A2; :: thesis: verum