YES
Time: 0.008830
TRS:
 {  minus(x, 0()) -> x,
  minus(s x, s y) -> minus(x, y),
       double 0() -> 0(),
       double s x -> s s double x,
     plus(0(), y) -> y,
     plus(s x, y) -> s plus(x, y),
     plus(s x, y) -> s plus(minus(x, y), double y),
     plus(s x, y) -> plus(x, s y)}
 DP:
  DP:
   {minus#(s x, s y) -> minus#(x, y),
         double# s x -> double# x,
       plus#(s x, y) -> minus#(x, y),
       plus#(s x, y) -> double# y,
       plus#(s x, y) -> plus#(x, y),
       plus#(s x, y) -> plus#(x, s y),
       plus#(s x, y) -> plus#(minus(x, y), double y)}
  TRS:
  {  minus(x, 0()) -> x,
   minus(s x, s y) -> minus(x, y),
        double 0() -> 0(),
        double s x -> s s double x,
      plus(0(), y) -> y,
      plus(s x, y) -> s plus(x, y),
      plus(s x, y) -> s plus(minus(x, y), double y),
      plus(s x, y) -> plus(x, s y)}
  EDG:
   {(plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(minus(x, y), double y))
    (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, y))
    (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> double# y)
    (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> minus#(x, y))
    (double# s x -> double# x, double# s x -> double# x)
    (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> double# y)
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(minus(x, y), double y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (plus#(s x, y) -> double# y, double# s x -> double# x)
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> minus#(x, y))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> double# y)
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, y))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y))}
   SCCS (3):
    Scc:
     {plus#(s x, y) -> plus#(x, y),
      plus#(s x, y) -> plus#(x, s y),
      plus#(s x, y) -> plus#(minus(x, y), double y)}
    Scc:
     {double# s x -> double# x}
    Scc:
     {minus#(s x, s y) -> minus#(x, y)}
    SCC (3):
     Strict:
      {plus#(s x, y) -> plus#(x, y),
       plus#(s x, y) -> plus#(x, s y),
       plus#(s x, y) -> plus#(minus(x, y), double y)}
     Weak:
     {  minus(x, 0()) -> x,
      minus(s x, s y) -> minus(x, y),
           double 0() -> 0(),
           double s x -> s s double x,
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(x, y),
         plus(s x, y) -> s plus(minus(x, y), double y),
         plus(s x, y) -> plus(x, s y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0,
       
       [plus](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [double](x0) = x0 + 1,
       
       [0] = 1,
       
       [plus#](x0, x1) = x0
      Strict:
       plus#(s x, y) -> plus#(minus(x, y), double y)
       1 + 1x + 0y >= 0 + 1x + 0y
       plus#(s x, y) -> plus#(x, s y)
       1 + 1x + 0y >= 0 + 1x + 0y
       plus#(s x, y) -> plus#(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       
     Qed
   SCC (1):
    Strict:
     {double# s x -> double# x}
    Weak:
    {  minus(x, 0()) -> x,
     minus(s x, s y) -> minus(x, y),
          double 0() -> 0(),
          double s x -> s s double x,
        plus(0(), y) -> y,
        plus(s x, y) -> s plus(x, y),
        plus(s x, y) -> s plus(minus(x, y), double y),
        plus(s x, y) -> plus(x, s y)}
    SPSC:
     Simple Projection:
      pi(double#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {minus#(s x, s y) -> minus#(x, y)}
    Weak:
    {  minus(x, 0()) -> x,
     minus(s x, s y) -> minus(x, y),
          double 0() -> 0(),
          double s x -> s s double x,
        plus(0(), y) -> y,
        plus(s x, y) -> s plus(x, y),
        plus(s x, y) -> s plus(minus(x, y), double y),
        plus(s x, y) -> plus(x, s y)}
    SPSC:
     Simple Projection:
      pi(minus#) = 1
     Strict:
      {}
     Qed