(VAR x y z)
(RULES
+(x,0) -> x
+(x,i(x)) -> 0
+(+(x,y),z) -> +(x,+(y,z))
*(x,+(y,z)) -> +(*(x,y),*(x,z))
*(+(x,y),z) -> +(*(x,z),*(y,z))
)
(COMMENT Example 4.9 (Ring) in \cite{SK90})