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