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