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

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