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