TRS:
 {        +(X, 0()) -> X,
         +(X, s(Y)) -> s(+(X, Y)),
  f(0(), s(0()), X) -> f(X, +(X, X), X),
            g(X, Y) -> X,
            g(X, Y) -> Y}
 Fail