YES
Time: 0.011561
TRS:
 {  double x -> +(x, x),
  double 0() -> 0(),
  double s x -> s s double x,
   +(x, 0()) -> x,
   +(x, s y) -> s +(x, y),
   +(s x, y) -> s +(x, y)}
 DP:
  DP:
   {  double# x -> +#(x, x),
    double# s x -> double# x,
     +#(x, s y) -> +#(x, y),
     +#(s x, y) -> +#(x, y)}
  TRS:
  {  double x -> +(x, x),
   double 0() -> 0(),
   double s x -> s s double x,
    +(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
    +(s x, y) -> s +(x, y)}
  UR:
   {a(z, w) -> z,
    a(z, w) -> w}
   EDG:
    {(+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (double# x -> +#(x, x), +#(s x, y) -> +#(x, y))
     (double# x -> +#(x, x), +#(x, s y) -> +#(x, y))
     (+#(s x, y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (double# s x -> double# x, double# x -> +#(x, x))
     (double# s x -> double# x, double# s x -> double# x)}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {double# s x -> double# x}
      Scc:
       {+#(x, s y) -> +#(x, y),
        +#(s x, y) -> +#(x, y)}
      
      SCC (1):
       Strict:
        {double# s x -> double# x}
       Weak:
       {  double x -> +(x, x),
        double 0() -> 0(),
        double s x -> s s double x,
         +(x, 0()) -> x,
         +(x, s y) -> s +(x, y),
         +(s x, y) -> s +(x, y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + x1 + 1,
         
         [double](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [double#](x0) = x0
        Strict:
         double# s x -> double# x
         1 + 1x >= 0 + 1x
        Weak:
         +(s x, y) -> s +(x, y)
         2 + 1x + 1y >= 2 + 1x + 1y
         +(x, s y) -> s +(x, y)
         2 + 1x + 1y >= 2 + 1x + 1y
         +(x, 0()) -> x
         2 + 1x >= 1x
         double s x -> s s double x
         2 + 1x >= 3 + 1x
         double 0() -> 0()
         2 >= 1
         double x -> +(x, x)
         1 + 1x >= 1 + 2x
       Qed
     
     SCC (2):
      Strict:
       {+#(x, s y) -> +#(x, y),
        +#(s x, y) -> +#(x, y)}
      Weak:
      {  double x -> +(x, x),
       double 0() -> 0(),
       double s x -> s s double x,
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y),
        +(s x, y) -> s +(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + x1 + 1,
        
        [double](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [+#](x0, x1) = x0
       Strict:
        +#(s x, y) -> +#(x, y)
        0 + 0x + 1y >= 0 + 0x + 1y
        +#(x, s y) -> +#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        +(s x, y) -> s +(x, y)
        2 + 1x + 1y >= 2 + 1x + 1y
        +(x, s y) -> s +(x, y)
        2 + 1x + 1y >= 2 + 1x + 1y
        +(x, 0()) -> x
        2 + 1x >= 1x
        double s x -> s s double x
        0 + 0x >= 2 + 0x
        double 0() -> 0()
        0 >= 1
        double x -> +(x, x)
        0 + 0x >= 1 + 2x
      SCCS (1):
       Scc:
        {+#(s x, y) -> +#(x, y)}
       
       SCC (1):
        Strict:
         {+#(s x, y) -> +#(x, y)}
        Weak:
        {  double x -> +(x, x),
         double 0() -> 0(),
         double s x -> s s double x,
          +(x, 0()) -> x,
          +(x, s y) -> s +(x, y),
          +(s x, y) -> s +(x, y)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [+](x0, x1) = x0 + x1 + 1,
          
          [double](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [0] = 1,
          
          [+#](x0, x1) = x0
         Strict:
          +#(s x, y) -> +#(x, y)
          1 + 1x + 0y >= 0 + 1x + 0y
         Weak:
          +(s x, y) -> s +(x, y)
          2 + 1x + 1y >= 2 + 1x + 1y
          +(x, s y) -> s +(x, y)
          2 + 1x + 1y >= 2 + 1x + 1y
          +(x, 0()) -> x
          2 + 1x >= 1x
          double s x -> s s double x
          2 + 1x >= 3 + 1x
          double 0() -> 0()
          2 >= 1
          double x -> +(x, x)
          1 + 1x >= 1 + 2x
        Qed