(VAR x y z) (RULES *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,1) -> x *(1,y) -> y ) (COMMENT Example 4.5 (Distributivity) in \cite{SK90})