(VAR x y z)
(RULES
f(0,y) -> y
f(x,0) -> x
f(i(x),y) -> i(x)
f(f(x,y),z) -> f(x,f(y,z))
f(g(x,y),z) -> g(f(x,z),f(y,z))
f(1,g(x,y)) -> x
f(2,g(x,y)) -> y
)
(COMMENT Example 2.7 in \cite{SK90})