YES

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

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