YES

Problem:
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 if(0(),y,z) -> y
 if(s(x),y,z) -> z
 half(double(x)) -> x

Proof:
 DP Processor:
  DPs:
   double#(s(x)) -> double#(x)
   half#(s(s(x))) -> half#(x)
   -#(s(x),s(y)) -> -#(x,y)
  TRS:
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
   if(0(),y,z) -> y
   if(s(x),y,z) -> z
   half(double(x)) -> x
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [-#](x0, x1) = 4x1,
    
    [half#](x0) = 2x0 + 1,
    
    [double#](x0) = 2x0 + 1,
    
    [if](x0, x1, x2) = x0 + 2x1 + 2x2 + 4,
    
    [-](x0, x1) = 4x0 + 2,
    
    [half](x0) = x0 + 1,
    
    [s](x0) = x0 + 4,
    
    [double](x0) = 4x0,
    
    [0] = 4
   orientation:
    double#(s(x)) = 2x + 9 >= 2x + 1 = double#(x)
    
    half#(s(s(x))) = 2x + 17 >= 2x + 1 = half#(x)
    
    -#(s(x),s(y)) = 4y + 16 >= 4y = -#(x,y)
    
    double(0()) = 16 >= 4 = 0()
    
    double(s(x)) = 4x + 16 >= 4x + 8 = s(s(double(x)))
    
    half(0()) = 5 >= 4 = 0()
    
    half(s(0())) = 9 >= 4 = 0()
    
    half(s(s(x))) = x + 9 >= x + 5 = s(half(x))
    
    -(x,0()) = 4x + 2 >= x = x
    
    -(s(x),s(y)) = 4x + 18 >= 4x + 2 = -(x,y)
    
    if(0(),y,z) = 2y + 2z + 8 >= y = y
    
    if(s(x),y,z) = x + 2y + 2z + 8 >= z = z
    
    half(double(x)) = 4x + 1 >= x = x
   problem:
    DPs:
     
    TRS:
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     if(0(),y,z) -> y
     if(s(x),y,z) -> z
     half(double(x)) -> x
   Qed