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