MAYBE
MAYBE
TRS:
 {
     +(x, +(y, z)) -> +(+(x, y), z),
         +(x, 0()) -> x,
        +(x, s(y)) -> s(+(x, y)),
         +(0(), y) -> y,
        +(s(x), y) -> s(+(x, y)),
  f(h(x, h(y, z))) -> f(h(+(x, y), z)),
        f(g(f(x))) -> f(h(s(0()), x)),
     f(g(h(x, y))) -> f(h(s(x), y))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
       +(x, +(y, z)) -> +(+(x, y), z),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y)),
           +(0(), y) -> y,
          +(s(x), y) -> s(+(x, y)),
    f(h(x, h(y, z))) -> f(h(+(x, y), z)),
          f(g(f(x))) -> f(h(s(0()), x)),
       f(g(h(x, y))) -> f(h(s(x), y))
   }
  Fail