YES

Problem:
 add(0(),x) -> x
 add(s(x),y) -> s(add(x,y))
 mult(0(),x) -> 0()
 mult(s(x),y) -> add(y,mult(x,y))

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