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)-bounded by 2
       Automaton:
        {         0_2() -> 3*
                  0_1() -> 3 | 1
                  0_0() -> 1*
                  1_1() -> 2*
                  1_0() -> 1*
         times#_1(1, 4) -> 1*
         times#_0(1, 1) -> 1*
          times_1(2, 1) -> 3*
          times_0(1, 1) -> 1*
           plus_1(1, 3) -> 4*
           plus_0(1, 1) -> 1*
                      1 -> 4*}
       Strict:
        {}
       Qed