(VAR x)
(RULES
  f0(c0, f0(c0, x)) -> f0(f0(c0, c0), c0)
)
(COMMENT NFP & ~CR)