MAYBE
Trs:
 {    f(0()) -> 1(),
     f(s(x)) -> g(x, s(x)),
   +(x, 0()) -> x,
  +(x, s(y)) -> s(+(x, y)),
   g(0(), y) -> y,
  g(s(x), y) -> g(x, +(y, s(x))),
  g(s(x), y) -> g(x, s(+(y, x)))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open