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
   
   interpretation:
    [times#](x0, x1) = 5x0 + 4x1,
    
    [plus#](x0, x1) = 4x0 + 2,
    
    [times](x0, x1) = 5x0 + x1 + 4,
    
    [s](x0) = 6x0 + 4,
    
    [plus](x0, x1) = 4x0 + x1 + 4
   orientation:
    plus#(plus(X,Y),Z) = 16X + 4Y + 18 >= 4Y + 2 = plus#(Y,Z)
    
    plus#(plus(X,Y),Z) = 16X + 4Y + 18 >= 4X + 2 = plus#(X,plus(Y,Z))
    
    times#(X,s(Y)) = 5X + 24Y + 16 >= 4X + 5Y = times#(Y,X)
    
    times#(X,s(Y)) = 5X + 24Y + 16 >= 4X + 2 = plus#(X,times(Y,X))
    
    plus(plus(X,Y),Z) = 16X + 4Y + Z + 20 >= 4X + 4Y + Z + 8 = plus(X,plus(Y,Z))
    
    times(X,s(Y)) = 5X + 6Y + 8 >= 5X + 5Y + 8 = 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