YES

Problem:
 times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x)
 times(x,1()) -> x
 plus(x,0()) -> x
 times(x,0()) -> 0()

Proof:
 DP Processor:
  DPs:
   times#(x,plus(y,1())) -> 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)
  TRS:
   times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x)
   times(x,1()) -> x
   plus(x,0()) -> x
   times(x,0()) -> 0()
  EDG Processor:
   DPs:
    times#(x,plus(y,1())) -> 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)
   TRS:
    times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x)
    times(x,1()) -> x
    plus(x,0()) -> x
    times(x,0()) -> 0()
   graph:
    times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) ->
    times#(x,plus(y,1())) -> times#(1(),0())
    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())) -> times#(x,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)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 4/16
    DPs:
     times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0())))
    TRS:
     times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x)
     times(x,1()) -> x
     plus(x,0()) -> x
     times(x,0()) -> 0()
    Usable Rule Processor:
     DPs:
      times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0())))
     TRS:
      times(x,0()) -> 0()
      plus(x,0()) -> x
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {6}
       transitions:
        times{#,0}(5,8) -> 6*
        plus0(3,1) -> 4*
        plus0(3,3) -> 4*
        plus0(4,2) -> 4*
        plus0(4,4) -> 4*
        plus0(5,7) -> 8*
        plus0(1,2) -> 4*
        plus0(1,4) -> 4*
        plus0(2,1) -> 4*
        plus0(2,3) -> 4*
        plus0(3,2) -> 4*
        plus0(3,4) -> 4*
        plus0(4,1) -> 4*
        plus0(4,3) -> 4*
        plus0(1,1) -> 4*
        plus0(1,3) -> 4*
        plus0(2,2) -> 4*
        plus0(2,4) -> 4*
        10() -> 3*
        times0(3,1) -> 7,2
        times0(3,3) -> 2*
        times0(4,2) -> 2*
        times0(4,4) -> 2*
        times0(1,2) -> 2*
        times0(1,4) -> 2*
        times0(2,1) -> 2*
        times0(2,3) -> 2*
        times0(3,2) -> 2*
        times0(3,4) -> 2*
        times0(4,1) -> 2*
        times0(4,3) -> 2*
        times0(1,1) -> 2*
        times0(1,3) -> 2*
        times0(2,2) -> 2*
        times0(2,4) -> 2*
        00() -> 7,2,1
        times{#,1}(5,16) -> 6*
        plus1(3,15) -> 16*
        plus1(4,15) -> 16*
        times1(14,13) -> 15*
        11() -> 14*
        01() -> 15,13
        1 -> 4,5
        2 -> 4,5
        3 -> 4,5
        4 -> 16,5
        5 -> 8*
      problem:
       DPs:
        
       TRS:
        times(x,0()) -> 0()
        plus(x,0()) -> x
      Qed