(VAR x y)
(RULES
*(x, \(x, y)) -> y
\(x, *(x, y)) -> y
/(*(x, y), y) -> x
*(/(x, y), y) -> x
*(x, *(y, x)) -> y
)