MAYBE

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()
  Open