(VAR x y z) (SIG (f0 2) (c0 0) (c1 0) (c2 0)) (RULES c0 -> c1 f0(x, c0) -> f0(c1, c1) f0(c1, x) -> f0(c1, c1) f0(f0(x, y), z) -> f0(c1, c1) ) (COMMENT Example 1 on p.28 of \cite{IWC16} with additional c2)