let R be Ring; :: thesis: for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = (IC s) + 1 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 ) = (IC s) + 1 implies not I is halting )
given s being State of (SCM R) such that A1: (Exec (I,s)) . (IC ) = (IC s) + 1 ; :: thesis: not I is halting
A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;
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 ) = w + 1 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;
hence contradiction by A3; :: thesis: verum