YES
TRS:
 {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
       times(X, s(Y)) -> plus(X, times(Y, X))}
 DP:
  Strict:
   {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
    plus#(plus(X, Y), Z) -> plus#(Y, Z),
         times#(X, s(Y)) -> plus#(X, times(Y, X)),
         times#(X, s(Y)) -> times#(Y, X)}
  Weak:
  {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
        times(X, s(Y)) -> plus(X, times(Y, X))}
  EDG:
   {(plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(Y, Z))
    (plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(Y, Z))
    (plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (times#(X, s(Y)) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (times#(X, s(Y)) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(Y, Z))
    (times#(X, s(Y)) -> times#(Y, X), times#(X, s(Y)) -> plus#(X, times(Y, X)))
    (times#(X, s(Y)) -> times#(Y, X), times#(X, s(Y)) -> times#(Y, X))}
   SCCS:
    Scc:
     {times#(X, s(Y)) -> times#(Y, X)}
    Scc:
     {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
      plus#(plus(X, Y), Z) -> plus#(Y, Z)}
    SCC:
     Strict:
      {times#(X, s(Y)) -> times#(Y, X)}
     Weak:
     {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
           times(X, s(Y)) -> plus(X, times(Y, X))}
     POLY:
      Argument Filtering:
       pi(s) = [0], pi(times#) = [0,1], pi(times) = [], pi(plus) = []
      Usable Rules:
       {}
      Interpretation:
       [times#](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
             times(X, s(Y)) -> plus(X, times(Y, X))}
      Qed
    SCC:
     Strict:
      {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
       plus#(plus(X, Y), Z) -> plus#(Y, Z)}
     Weak:
     {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
           times(X, s(Y)) -> plus(X, times(Y, X))}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
      EDG:
       {(plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(Y, Z))}
       SCCS:
        Scc:
         {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
        SCC:
         Strict:
          {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
         Weak:
         {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
               times(X, s(Y)) -> plus(X, times(Y, X))}
         SPSC:
          Simple Projection:
           pi(plus#) = 0
          Strict:
           {}
          Qed