let I be Instruction of SCM+FSA; :: thesis: ( ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting )
given s being State of SCM+FSA such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; :: 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 Element of NAT ;
assume I is halting ; :: thesis: contradiction
then A2: (Exec (I,s)) . (IC ) = T . NAT by Th7, EXTPRO_1:def 3;
(Exec (I,s)) . (IC ) = succ w by A1, FUNCT_7:def 1, SCMFSA_1:5;
hence contradiction by A2; :: thesis: verum