(VAR x y z)
(RULES
f(f(x)) -> x
+(f(x), f(y)) -> f(+(x, y))
+(+(x, y), z) -> +(x, +(y, z))
)
(COMMENT Example 3.2 in \cite{SK90})