let I be Instruction of SCM+FSA ; :: thesis: ( ex s being State of SCM+FSA st (Exec I,s) . (IC SCM+FSA ) = Next implies not I is halting )
given s being State of SCM+FSA such that A1: (Exec I,s) . (IC SCM+FSA ) = Next ; :: thesis: not I is halting
assume A2: I is halting ; :: thesis: contradiction
reconsider T = s as SCM+FSA-State ;
A3: IC T = T . NAT ;
A4: (Exec I,s) . (IC SCM+FSA ) = T . NAT by A2, Th7, AMI_1:def 8;
reconsider w = T . NAT as Instruction-Location of SCM+FSA by A3, AMI_1:def 4;
(Exec I,s) . (IC SCM+FSA ) = Next by A1, FUNCT_7:def 1, SCMFSA_1:5;
hence contradiction by A4; :: thesis: verum