YES

Problem:
 sqr(0()) -> 0()
 sqr(s(x)) -> +(sqr(x),s(double(x)))
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 sqr(s(x)) -> s(+(sqr(x),double(x)))

Proof:
 DP Processor:
  DPs:
   sqr#(s(x)) -> double#(x)
   sqr#(s(x)) -> sqr#(x)
   sqr#(s(x)) -> +#(sqr(x),s(double(x)))
   double#(s(x)) -> double#(x)
   +#(x,s(y)) -> +#(x,y)
   sqr#(s(x)) -> +#(sqr(x),double(x))
  TRS:
   sqr(0()) -> 0()
   sqr(s(x)) -> +(sqr(x),s(double(x)))
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   sqr(s(x)) -> s(+(sqr(x),double(x)))
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
   interpretation:
    [+#](x0, x1) = x1 + 4,
    
    [double#](x0) = x0 + 4,
    
    [sqr#](x0) = 3x0 + 7,
    
    [+](x0, x1) = x0,
    
    [double](x0) = 3x0,
    
    [s](x0) = x0 + 1,
    
    [sqr](x0) = x0 + 5,
    
    [0] = 6
   orientation:
    sqr#(s(x)) = 3x + 10 >= x + 4 = double#(x)
    
    sqr#(s(x)) = 3x + 10 >= 3x + 7 = sqr#(x)
    
    sqr#(s(x)) = 3x + 10 >= 3x + 5 = +#(sqr(x),s(double(x)))
    
    double#(s(x)) = x + 5 >= x + 4 = double#(x)
    
    +#(x,s(y)) = y + 5 >= y + 4 = +#(x,y)
    
    sqr#(s(x)) = 3x + 10 >= 3x + 4 = +#(sqr(x),double(x))
    
    sqr(0()) = 11 >= 6 = 0()
    
    sqr(s(x)) = x + 6 >= x + 5 = +(sqr(x),s(double(x)))
    
    double(0()) = 18 >= 6 = 0()
    
    double(s(x)) = 3x + 3 >= 3x + 2 = s(s(double(x)))
    
    +(x,0()) = x >= x = x
    
    +(x,s(y)) = x >= x + 1 = s(+(x,y))
    
    sqr(s(x)) = x + 6 >= x + 6 = s(+(sqr(x),double(x)))
   problem:
    DPs:
     
    TRS:
     sqr(0()) -> 0()
     sqr(s(x)) -> +(sqr(x),s(double(x)))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     +(x,0()) -> x
     +(x,s(y)) -> s(+(x,y))
     sqr(s(x)) -> s(+(sqr(x),double(x)))
   Qed