YES
TRS:
 {          plus(x, s(y)) -> s(plus(x, y)),
             plus(x, 0()) -> x,
  times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
           times(x, s(y)) -> plus(times(x, y), x),
            times(x, 0()) -> 0()}
 DP:
  Strict:
   {          plus#(x, s(y)) -> plus#(x, y),
    times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())),
    times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
    times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
    times#(x, plus(y, s(z))) -> times#(x, s(z)),
    times#(x, plus(y, s(z))) -> times#(s(z), 0()),
             times#(x, s(y)) -> plus#(times(x, y), x),
             times#(x, s(y)) -> times#(x, y)}
  Weak:
  {          plus(x, s(y)) -> s(plus(x, y)),
              plus(x, 0()) -> x,
   times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
            times(x, s(y)) -> plus(times(x, y), x),
             times(x, 0()) -> 0()}
  EDG:
   {(times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, s(y)) -> times#(x, y))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(s(z), 0()))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(x, s(z)))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(x, s(y)) -> plus#(x, y))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(x, s(y)) -> plus#(x, y))
    (times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> times#(x, y))
    (times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(s(z), 0()))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(x, s(z)))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())))
    (plus#(x, s(y)) -> plus#(x, y), plus#(x, s(y)) -> plus#(x, y))
    (times#(x, plus(y, s(z))) -> times#(x, s(z)), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, plus(y, s(z))) -> times#(x, s(z)), times#(x, s(y)) -> times#(x, y))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(x, s(y)) -> plus#(x, y))}
   SCCS:
    Scc:
     {times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
      times#(x, plus(y, s(z))) -> times#(x, s(z)),
               times#(x, s(y)) -> times#(x, y)}
    Scc:
     {plus#(x, s(y)) -> plus#(x, y)}
    SCC:
     Strict:
      {times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
       times#(x, plus(y, s(z))) -> times#(x, s(z)),
                times#(x, s(y)) -> times#(x, y)}
     Weak:
     {          plus(x, s(y)) -> s(plus(x, y)),
                 plus(x, 0()) -> x,
      times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
               times(x, s(y)) -> plus(times(x, y), x),
                times(x, 0()) -> 0()}
     UR:
      {plus(x, s(y)) -> s(plus(x, y)),
        plus(x, 0()) -> x,
       times(x, 0()) -> 0()}
      BOUND:
       Bound: match(-raise)-bounded by 1
       Automaton:
        {         a_0() -> 1*
                  0_1() -> 6*
                  0_0() -> 6 | 5
                s_0(10) -> 9*
                 s_0(1) -> 4*
         times#_1(1, 1) -> 8*
         times#_0(1, 7) -> 3*
         times#_0(1, 4) -> 8*
         times#_0(1, 1) -> 8 | 2
          times_0(4, 5) -> 6*
           plus_0(1, 6) -> 7*
           plus_0(1, 1) -> 10*
                      9 -> 10*
                      8 -> 3 | 2
                      3 -> 8 | 2
                      1 -> 10 | 7}
       Strict:
        {}
       Qed
    SCC:
     Strict:
      {plus#(x, s(y)) -> plus#(x, y)}
     Weak:
     {          plus(x, s(y)) -> s(plus(x, y)),
                 plus(x, 0()) -> x,
      times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
               times(x, s(y)) -> plus(times(x, y), x),
                times(x, 0()) -> 0()}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed