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