NO

1 decompositions
 #0 -----------
   1: plus(x,0()) -> x
   2: plus(0(),1()) -> 1()
   3: plus(x,plus(y,1())) -> plus(plus(x,y),1())
   4: times(x,0()) -> 0()
   5: times(x,1()) -> x
   6: times(x,plus(y,1())) -> plus(times(x,y),x)
   7: m(0()) -> 0()
   8: plus(m(1()),1()) -> 0()
   9: plus(m(plus(x,1())),1()) -> m(x)
  10: m(m(x)) -> x
  11: plus(x,m(y)) -> m(plus(m(x),y))
  12: times(x,m(y)) -> m(times(x,y))

unjoinable peak
    _y19
*<- times(_y19,plus(0(),1())) ->*
    plus(times(_y19,0()),_y19)