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