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