TRS:
 {    f(0()) -> 1(),
     f(s(x)) -> g(x, s(x)),
   g(0(), y) -> y,
  g(s(x), y) -> g(x, +(y, s(x))),
   +(x, 0()) -> x,
  +(x, s(y)) -> s(+(x, y)),
  g(s(x), y) -> g(x, s(+(y, x)))}
 Fail