(VAR x y)
(RULES
*(x, \(x, y)) -> y
\(x, *(x, y)) -> y
/(*(x, y), y) -> x
*(/(x, y), y) -> x
*(x, *(y, x)) -> y
)
(COMMENT Example 3.8 in \cite{SK90})