let R be good Ring; :: thesis: for I being Instruction of (SCM R) st I is halting holds
I = halt (SCM R)
let I be Instruction of (SCM R); :: thesis: ( I is halting implies I = halt (SCM R) )
assume I is halting ; :: thesis: I = halt (SCM R)
then I = [0,{},{}] by Lm8;
hence I = halt (SCM R) by Lm8; :: thesis: verum