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