MAYBE
Time: 0.010064
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:
  DP:
   {       +#(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)}
  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}
  UR:
   {+(X, 0()) -> X,
    +(X, s Y) -> s +(X, Y),
     double X -> +(X, X)}
   EDG:
    {(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)
     (double# X -> +#(X, X), +#(X, s Y) -> +#(X, Y))
     (+#(X, s Y) -> +#(X, Y), +#(X, s Y) -> +#(X, Y))
     (f#(0(), s 0(), X) -> double# X, double# X -> +#(X, X))}
    STATUS:
     arrows: 0.687500
     SCCS (2):
      Scc:
       {f#(0(), s 0(), X) -> f#(X, double X, X)}
      Scc:
       {+#(X, s Y) -> +#(X, Y)}
      
      SCC (1):
       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}
       Open
      
      
      SCC (1):
       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}
       Open