YES

Problem:
 plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
 times(X,s(Y)) -> plus(X,times(Y,X))

Proof:
 DP Processor:
  DPs:
   plus#(plus(X,Y),Z) -> plus#(Y,Z)
   plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z))
   times#(X,s(Y)) -> times#(Y,X)
   times#(X,s(Y)) -> plus#(X,times(Y,X))
  TRS:
   plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
   times(X,s(Y)) -> plus(X,times(Y,X))
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    
   interpretation:
    [times#](x0, x1) = x0 + x1 + 2,
    
    [plus#](x0, x1) = x0 + 4,
    
    [times](x0, x1) = 4x1,
    
    [s](x0) = x0 + 4,
    
    [plus](x0, x1) = 2x0 + x1 + 1
   orientation:
    plus#(plus(X,Y),Z) = 2X + Y + 5 >= Y + 4 = plus#(Y,Z)
    
    plus#(plus(X,Y),Z) = 2X + Y + 5 >= X + 4 = plus#(X,plus(Y,Z))
    
    times#(X,s(Y)) = X + Y + 6 >= X + Y + 2 = times#(Y,X)
    
    times#(X,s(Y)) = X + Y + 6 >= X + 4 = plus#(X,times(Y,X))
    
    plus(plus(X,Y),Z) = 4X + 2Y + Z + 3 >= 2X + 2Y + Z + 2 = plus(X,plus(Y,Z))
    
    times(X,s(Y)) = 4Y + 16 >= 6X + 1 = plus(X,times(Y,X))
   problem:
    DPs:
     
    TRS:
     plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
     times(X,s(Y)) -> plus(X,times(Y,X))
   Qed