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