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