YES

Problem:
 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) -> plus(x,s(y))
 plus(s(x),y) -> s(plus(minus(x,y),double(y)))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   double#(s(x)) -> double#(x)
   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) -> minus#(x,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) -> plus(x,s(y))
   plus(s(x),y) -> s(plus(minus(x,y),double(y)))
  TDG Processor:
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    double#(s(x)) -> double#(x)
    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) -> minus#(x,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) -> plus(x,s(y))
    plus(s(x),y) -> s(plus(minus(x,y),double(y)))
   graph:
    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) -> 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,s(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#(minus(x,y),double(y))
    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,s(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#(minus(x,y),double(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,s(y))
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
    plus#(s(x),y) -> double#(y) -> double#(s(x)) -> double#(x)
    plus#(s(x),y) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
    double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 19/49
    DPs:
     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))
    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) -> plus(x,s(y))
     plus(s(x),y) -> s(plus(minus(x,y),double(y)))
    Usable Rule Processor:
     DPs:
      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))
     TRS:
      double(0()) -> 0()
      double(s(x)) -> s(s(double(x)))
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
      interpretation:
       [plus#](x0, x1) = 4x0,
       
       [double](x0) = 3x0 + 4,
       
       [s](x0) = 1x0 + 0,
       
       [minus](x0, x1) = 1x0 + 0,
       
       [0] = 3
      orientation:
       plus#(s(x),y) = 5x + 4 >= 5x + 4 = plus#(minus(x,y),double(y))
       
       plus#(s(x),y) = 5x + 4 >= 4x = plus#(x,y)
       
       plus#(s(x),y) = 5x + 4 >= 4x = plus#(x,s(y))
       
       double(0()) = 6 >= 3 = 0()
       
       double(s(x)) = 4x + 4 >= 5x + 6 = s(s(double(x)))
       
       minus(x,0()) = 1x + 0 >= x = x
       
       minus(s(x),s(y)) = 2x + 1 >= 1x + 0 = minus(x,y)
      problem:
       DPs:
        plus#(s(x),y) -> plus#(minus(x,y),double(y))
        plus#(s(x),y) -> plus#(x,y)
       TRS:
        double(0()) -> 0()
        double(s(x)) -> s(s(double(x)))
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
      Restore Modifier:
       DPs:
        plus#(s(x),y) -> plus#(minus(x,y),double(y))
        plus#(s(x),y) -> plus#(x,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) -> plus(x,s(y))
        plus(s(x),y) -> s(plus(minus(x,y),double(y)))
       Usable Rule Processor:
        DPs:
         plus#(s(x),y) -> plus#(minus(x,y),double(y))
         plus#(s(x),y) -> plus#(x,y)
        TRS:
         double(0()) -> 0()
         double(s(x)) -> s(s(double(x)))
         minus(x,0()) -> x
         minus(s(x),s(y)) -> minus(x,y)
        Arctic Interpretation Processor:
         dimension: 1
         usable rules:
          minus(x,0()) -> x
          minus(s(x),s(y)) -> minus(x,y)
         interpretation:
          [plus#](x0, x1) = 4x0,
          
          [double](x0) = x0 + 1,
          
          [s](x0) = 1x0,
          
          [minus](x0, x1) = x0,
          
          [0] = 0
         orientation:
          plus#(s(x),y) = 5x >= 4x = plus#(minus(x,y),double(y))
          
          plus#(s(x),y) = 5x >= 4x = plus#(x,y)
          
          double(0()) = 1 >= 0 = 0()
          
          double(s(x)) = 1x + 1 >= 2x + 3 = s(s(double(x)))
          
          minus(x,0()) = x >= x = x
          
          minus(s(x),s(y)) = 1x >= x = minus(x,y)
         problem:
          DPs:
           plus#(s(x),y) -> plus#(x,y)
          TRS:
           double(0()) -> 0()
           double(s(x)) -> s(s(double(x)))
           minus(x,0()) -> x
           minus(s(x),s(y)) -> minus(x,y)
         Restore Modifier:
          DPs:
           plus#(s(x),y) -> plus#(x,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) -> plus(x,s(y))
           plus(s(x),y) -> s(plus(minus(x,y),double(y)))
          Subterm Criterion Processor:
           simple projection:
            pi(plus#) = 0
           problem:
            DPs:
             
            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) -> plus(x,s(y))
             plus(s(x),y) -> s(plus(minus(x,y),double(y)))
           Qed
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,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) -> plus(x,s(y))
     plus(s(x),y) -> s(plus(minus(x,y),double(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(minus#) = 1
     problem:
      DPs:
       
      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) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(minus(x,y),double(y)))
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    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) -> plus(x,s(y))
     plus(s(x),y) -> s(plus(minus(x,y),double(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      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) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(minus(x,y),double(y)))
     Qed