let R be Ring; :: thesis: [0,{},{}] is Instruction of (SCM R)
halt (SCM R) = [0,{},{}] ;
hence [0,{},{}] is Instruction of (SCM R) ; :: thesis: verum