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 1
       Automaton:
        {           0_1() -> 17 | 16
                    0_0() -> 13 | 11 | 10
                    1_1() -> 15*
                    1_0() -> 12*
          times#_1(9, 18) -> 6*
         times#_0(14, 14) -> 6*
         times#_0(13, 14) -> 6*
         times#_0(12, 14) -> 6*
         times#_0(11, 14) -> 6*
         times#_0(10, 14) -> 6*
          times#_0(9, 14) -> 6*
          times_1(15, 16) -> 17*
          times_0(14, 14) -> 10*
          times_0(14, 13) -> 10*
          times_0(14, 12) -> 10*
          times_0(14, 11) -> 10*
          times_0(14, 10) -> 10*
           times_0(14, 9) -> 10*
          times_0(13, 14) -> 10*
          times_0(13, 13) -> 10*
          times_0(13, 12) -> 10*
          times_0(13, 11) -> 10*
          times_0(13, 10) -> 10*
           times_0(13, 9) -> 10*
          times_0(12, 14) -> 10*
          times_0(12, 13) -> 11*
          times_0(12, 12) -> 10*
          times_0(12, 11) -> 10*
          times_0(12, 10) -> 10*
           times_0(12, 9) -> 10*
          times_0(11, 14) -> 10*
          times_0(11, 13) -> 10*
          times_0(11, 12) -> 10*
          times_0(11, 11) -> 10*
          times_0(11, 10) -> 10*
           times_0(11, 9) -> 10*
          times_0(10, 14) -> 10*
          times_0(10, 13) -> 10*
          times_0(10, 12) -> 10*
          times_0(10, 11) -> 10*
          times_0(10, 10) -> 10*
           times_0(10, 9) -> 10*
           times_0(9, 14) -> 10*
           times_0(9, 13) -> 10*
           times_0(9, 12) -> 10*
           times_0(9, 11) -> 10*
           times_0(9, 10) -> 10*
            times_0(9, 9) -> 10*
            plus_1(9, 17) -> 18*
           plus_0(14, 14) -> 9*
           plus_0(14, 13) -> 9*
           plus_0(14, 12) -> 9*
           plus_0(14, 11) -> 14*
           plus_0(14, 10) -> 9*
            plus_0(14, 9) -> 9*
           plus_0(13, 14) -> 9*
           plus_0(13, 13) -> 9*
           plus_0(13, 12) -> 9*
           plus_0(13, 11) -> 14*
           plus_0(13, 10) -> 9*
            plus_0(13, 9) -> 9*
           plus_0(12, 14) -> 9*
           plus_0(12, 13) -> 9*
           plus_0(12, 12) -> 9*
           plus_0(12, 11) -> 14*
           plus_0(12, 10) -> 9*
            plus_0(12, 9) -> 9*
           plus_0(11, 14) -> 9*
           plus_0(11, 13) -> 9*
           plus_0(11, 12) -> 9*
           plus_0(11, 11) -> 14*
           plus_0(11, 10) -> 9*
            plus_0(11, 9) -> 9*
           plus_0(10, 14) -> 9*
           plus_0(10, 13) -> 9*
           plus_0(10, 12) -> 9*
           plus_0(10, 11) -> 14*
           plus_0(10, 10) -> 9*
            plus_0(10, 9) -> 9*
            plus_0(9, 14) -> 9*
            plus_0(9, 13) -> 9*
            plus_0(9, 12) -> 9*
            plus_0(9, 11) -> 14*
            plus_0(9, 10) -> 9*
             plus_0(9, 9) -> 9*
                       14 -> 9*
                       13 -> 9*
                       12 -> 9*
                       11 -> 9*
                       10 -> 9*
                        9 -> 18 | 14}
       Strict:
        {}
       Qed