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 ) = succ (IC s) 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 ) = succ (IC s) implies not I is halting )
given s being State of (SCM R) such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; :: thesis: not I is halting
A2: the Object-Kind of (SCM R) = SCM-OK R by Def1;
reconsider t = s as SCM-State of R by A2, CARD_3:107;
IC t = t . NAT ;
then reconsider w = t . NAT as Element of NAT ;
A3: (Exec (I,s)) . (IC ) = succ w by A1, Def1;
assume A4: I is halting ; :: thesis: contradiction
IC t = IC s by Def1;
then (Exec (I,s)) . (IC ) = t . NAT by A4, EXTPRO_1:def 3;
hence contradiction by A3; :: thesis: verum