(VAR x y z)
(RULES
*(x, *(y, z)) -> *(*(x, y), z)
*(1, 1) -> 1
*(x, i(x)) -> 1
g(*(x, y), y) -> f(*(x, y), x)
f(1, y) -> y
)