(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 ) (COMMENT Example 3.6 in \cite{SK90})