let R be good Ring; :: thesis: InsCode (halt (SCM R)) = 0
thus InsCode (halt (SCM R)) = [0 ,{} ,{} ] `1_3 by SCMRING2:30
.= 0 by RECDEF_2:def 1 ; :: thesis: verum