MAYBE
TRS:
 {        +(X, 0()) -> X,
         +(X, s(Y)) -> s(+(X, Y)),
          double(X) -> +(X, X),
  f(0(), s(0()), X) -> f(X, double(X), X),
            g(X, Y) -> X,
            g(X, Y) -> Y}
 DP:
  Strict:
   {       +#(X, s(Y)) -> +#(X, Y),
            double#(X) -> +#(X, X),
    f#(0(), s(0()), X) -> double#(X),
    f#(0(), s(0()), X) -> f#(X, double(X), X)}
  Weak:
  {        +(X, 0()) -> X,
          +(X, s(Y)) -> s(+(X, Y)),
           double(X) -> +(X, X),
   f(0(), s(0()), X) -> f(X, double(X), X),
             g(X, Y) -> X,
             g(X, Y) -> Y}
  EDG:
   {(f#(0(), s(0()), X) -> double#(X), double#(X) -> +#(X, X))
    (f#(0(), s(0()), X) -> f#(X, double(X), X), f#(0(), s(0()), X) -> f#(X, double(X), X))
    (f#(0(), s(0()), X) -> f#(X, double(X), X), f#(0(), s(0()), X) -> double#(X))
    (+#(X, s(Y)) -> +#(X, Y), +#(X, s(Y)) -> +#(X, Y))
    (double#(X) -> +#(X, X), +#(X, s(Y)) -> +#(X, Y))}
   SCCS:
    Scc:
     {f#(0(), s(0()), X) -> f#(X, double(X), X)}
    Scc:
     {+#(X, s(Y)) -> +#(X, Y)}
    SCC:
     Strict:
      {f#(0(), s(0()), X) -> f#(X, double(X), X)}
     Weak:
     {        +(X, 0()) -> X,
             +(X, s(Y)) -> s(+(X, Y)),
              double(X) -> +(X, X),
      f(0(), s(0()), X) -> f(X, double(X), X),
                g(X, Y) -> X,
                g(X, Y) -> Y}
     Fail
    SCC:
     Strict:
      {+#(X, s(Y)) -> +#(X, Y)}
     Weak:
     {        +(X, 0()) -> X,
             +(X, s(Y)) -> s(+(X, Y)),
              double(X) -> +(X, X),
      f(0(), s(0()), X) -> f(X, double(X), X),
                g(X, Y) -> X,
                g(X, Y) -> Y}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed