let R be good Ring; :: thesis: halt (SCM R) = [0,{},{}]
reconsider I = [0,{},{}] as Instruction of (SCM R) by Th3;
I is halting by Th21;
hence halt (SCM R) = [0,{},{}] by Th29; :: thesis: verum