(VAR x y z)
(RULES
/(x, x) -> 1
/(x, 1) -> x
i(/(x, y)) -> /(y, x)
/(/(x, y), z) -> /(x, /(z, i(x)))
)
(COMMENT Example 3.12 in \cite{SK90})