MAYBE
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)),
  plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))}
 DP:
  Strict:
   {     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)),
    plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z)}
  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)),
   plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))}
  EDG:
   {(plus#(s(x), y) -> double#(y), double#(s(x)) -> double#(x))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(s(x), y) -> plus#(minus(x, y), double(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#(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) -> minus#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(minus(x, y), double(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#(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) -> minus#(x, y))
    (plus#(s(x), y) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (plus#(s(x), y) -> plus#(minus(x, y), double(y)), plus#(s(x), y) -> minus#(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) -> plus#(x, 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#(minus(x, y), double(y)))
    (plus#(s(x), y) -> plus#(minus(x, y), double(y)), plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z))
    (double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(x), y) -> minus#(x, y))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(x), y) -> double#(y))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(x), y) -> plus#(x, y))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(x), y) -> plus#(x, s(y)))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(x), y) -> plus#(minus(x, y), double(y)))
    (plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z), plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z))}
   SCCS:
    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)),
      plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z)}
    Scc:
     {double#(s(x)) -> double#(x)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     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)),
       plus#(s(plus(x, y)), z) -> plus#(plus(x, y), z)}
     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)),
      plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))}
     Fail
    SCC:
     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)),
      plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)),
      plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed