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)-DP-bounded by 1
       Automaton:
        {           0_1() -> 19 | 18
                    0_0() -> 15 | 13 | 11
                  s_1(10) -> 17*
                  s_0(16) -> 14*
                  s_0(15) -> 14*
                  s_0(14) -> 14*
                  s_0(13) -> 14*
                  s_0(11) -> 14*
                  s_0(10) -> 14*
         times#_1(10, 20) -> 6*
         times#_1(10, 17) -> 6*
         times#_0(16, 16) -> 6*
         times#_0(15, 16) -> 6*
         times#_0(14, 16) -> 6*
         times#_0(13, 16) -> 6*
         times#_0(11, 16) -> 6*
         times#_0(10, 16) -> 6*
          times_1(17, 18) -> 19*
          times_0(16, 16) -> 11*
          times_0(16, 15) -> 11*
          times_0(16, 14) -> 11*
          times_0(16, 13) -> 11*
          times_0(16, 11) -> 11*
          times_0(16, 10) -> 11*
          times_0(15, 16) -> 11*
          times_0(15, 15) -> 11*
          times_0(15, 14) -> 11*
          times_0(15, 13) -> 11*
          times_0(15, 11) -> 11*
          times_0(15, 10) -> 11*
          times_0(14, 16) -> 11*
          times_0(14, 15) -> 11*
          times_0(14, 14) -> 11*
          times_0(14, 13) -> 15*
          times_0(14, 11) -> 11*
          times_0(14, 10) -> 11*
          times_0(13, 16) -> 11*
          times_0(13, 15) -> 11*
          times_0(13, 14) -> 11*
          times_0(13, 13) -> 11*
          times_0(13, 11) -> 11*
          times_0(13, 10) -> 11*
          times_0(11, 16) -> 11*
          times_0(11, 15) -> 11*
          times_0(11, 14) -> 11*
          times_0(11, 13) -> 11*
          times_0(11, 11) -> 11*
          times_0(11, 10) -> 11*
          times_0(10, 16) -> 11*
          times_0(10, 15) -> 11*
          times_0(10, 14) -> 11*
          times_0(10, 13) -> 11*
          times_0(10, 11) -> 11*
          times_0(10, 10) -> 11*
           plus_1(10, 19) -> 20*
           plus_0(16, 16) -> 10*
           plus_0(16, 15) -> 16*
           plus_0(16, 14) -> 10*
           plus_0(16, 13) -> 10*
           plus_0(16, 11) -> 10*
           plus_0(16, 10) -> 10*
           plus_0(15, 16) -> 10*
           plus_0(15, 15) -> 16*
           plus_0(15, 14) -> 10*
           plus_0(15, 13) -> 10*
           plus_0(15, 11) -> 10*
           plus_0(15, 10) -> 10*
           plus_0(14, 16) -> 10*
           plus_0(14, 15) -> 16*
           plus_0(14, 14) -> 10*
           plus_0(14, 13) -> 10*
           plus_0(14, 11) -> 10*
           plus_0(14, 10) -> 10*
           plus_0(13, 16) -> 10*
           plus_0(13, 15) -> 16*
           plus_0(13, 14) -> 10*
           plus_0(13, 13) -> 10*
           plus_0(13, 11) -> 10*
           plus_0(13, 10) -> 10*
           plus_0(11, 16) -> 10*
           plus_0(11, 15) -> 16*
           plus_0(11, 14) -> 10*
           plus_0(11, 13) -> 10*
           plus_0(11, 11) -> 10*
           plus_0(11, 10) -> 10*
           plus_0(10, 16) -> 10*
           plus_0(10, 15) -> 16*
           plus_0(10, 14) -> 10*
           plus_0(10, 13) -> 10*
           plus_0(10, 11) -> 10*
           plus_0(10, 10) -> 10*
                       16 -> 10*
                       15 -> 10*
                       14 -> 10*
                       13 -> 10*
                       11 -> 10*
                       10 -> 20 | 16}
       Strict:
        {times#(x, plus(y, s(z))) -> times#(x, s(z)),
                  times#(x, s(y)) -> times#(x, y)}
       EDG:
        {(times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> times#(x, y))
         (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(x, s(z)))
         (times#(x, plus(y, s(z))) -> times#(x, s(z)), times#(x, s(y)) -> times#(x, y))}
        SCCS:
         Scc:
          {times#(x, plus(y, s(z))) -> times#(x, s(z)),
                    times#(x, s(y)) -> times#(x, y)}
         SCC:
          Strict:
           {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()}
          SPSC:
           Simple Projection:
            pi(times#) = 1
           Strict:
            {times#(x, s(y)) -> times#(x, y)}
           EDG:
            {(times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> times#(x, y))}
            SCCS:
             Scc:
              {times#(x, s(y)) -> times#(x, y)}
             SCC:
              Strict:
               {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()}
              SPSC:
               Simple Projection:
                pi(times#) = 1
               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