let R be good Ring; :: thesis: for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec I,s) . (IC (SCM R)) = Next holds
not I is halting
let I be Instruction of (SCM R); :: thesis: ( ex s being State of (SCM R) st (Exec I,s) . (IC (SCM R)) = Next implies not I is halting )
given s being State of (SCM R) such that A1: (Exec I,s) . (IC (SCM R)) = Next ; :: thesis: not I is halting
assume A2: I is halting ; :: thesis: contradiction
reconsider t = s as SCM-State of R by Def1;
A3: IC t = IC s by Def1;
A4: IC t = t . NAT ;
A5: (Exec I,s) . (IC (SCM R)) = t . NAT by A2, A3, AMI_1:def 8;
reconsider w = t . NAT as Instruction-Location of SCM R by A4, AMI_1:def 4;
(Exec I,s) . (IC (SCM R)) = Next by A1, Def1;
hence contradiction by A5; :: thesis: verum