YES
TRS:
 {          plus(x, 0()) -> x,
  times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
           times(x, 1()) -> x,
           times(x, 0()) -> 0()}
 DP:
  Strict:
   {times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())),
    times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x),
    times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))),
    times#(x, plus(y, 1())) -> times#(1(), 0())}
  Weak:
  {          plus(x, 0()) -> x,
   times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
            times(x, 1()) -> x,
            times(x, 0()) -> 0()}
  EDG:
   {(times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> times#(1(), 0()))}
   SCCS:
    Scc:
     {times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0())))}
    SCC:
     Strict:
      {times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0())))}
     Weak:
     {          plus(x, 0()) -> x,
      times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
               times(x, 1()) -> x,
               times(x, 0()) -> 0()}
     UR:
      { plus(x, 0()) -> x,
       times(x, 0()) -> 0()}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {         a_0() -> 2*
                  0_0() -> 5 | 4
                  1_0() -> 3*
         times#_0(2, 6) -> 1*
          times_0(3, 4) -> 5*
           plus_0(2, 5) -> 6*
                      2 -> 6*}
       Strict:
        {}
       Qed