YES
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:
  Strict:
   {   double#(x) -> +#(x, x),
    double#(s(x)) -> double#(x),
      +#(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))}
  EDG:
   {(double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
    (double#(s(x)) -> double#(x), double#(x) -> +#(x, x))
    (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
    (+#(s(x), y) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(s(x), y) -> +#(x, y))
    (double#(x) -> +#(x, x), +#(x, s(y)) -> +#(x, y))
    (double#(x) -> +#(x, x), +#(s(x), y) -> +#(x, y))}
   SCCS:
    Scc:
     {+#(x, s(y)) -> +#(x, y),
      +#(s(x), y) -> +#(x, y)}
    Scc:
     {double#(s(x)) -> double#(x)}
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {+#(x, s(y)) -> +#(x, y)}
      EDG:
       {(+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))}
       SCCS:
        Scc:
         {+#(x, s(y)) -> +#(x, y)}
        SCC:
         Strict:
          {+#(x, s(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))}
         SPSC:
          Simple Projection:
           pi(+#) = 1
          Strict:
           {}
          Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed