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