MAYBE

Problem:
 +(x,0()) -> x
 +(0(),x) -> x
 +(s(x),s(y)) -> s(s(+(x,y)))
 +(+(x,y),z) -> +(x,+(y,z))
 *(x,0()) -> 0()
 *(0(),x) -> 0()
 *(s(x),s(y)) -> s(+(*(x,y),+(x,y)))
 *(*(x,y),z) -> *(x,*(y,z))
 sum(nil()) -> 0()
 sum(cons(x,l)) -> +(x,sum(l))
 prod(nil()) -> s(0())
 prod(cons(x,l)) -> *(x,prod(l))

Proof:
 DP Processor:
  DPs:
   +#(s(x),s(y)) -> +#(x,y)
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   *#(s(x),s(y)) -> +#(x,y)
   *#(s(x),s(y)) -> *#(x,y)
   *#(s(x),s(y)) -> +#(*(x,y),+(x,y))
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
   sum#(cons(x,l)) -> sum#(l)
   sum#(cons(x,l)) -> +#(x,sum(l))
   prod#(cons(x,l)) -> prod#(l)
   prod#(cons(x,l)) -> *#(x,prod(l))
  TRS:
   +(x,0()) -> x
   +(0(),x) -> x
   +(s(x),s(y)) -> s(s(+(x,y)))
   +(+(x,y),z) -> +(x,+(y,z))
   *(x,0()) -> 0()
   *(0(),x) -> 0()
   *(s(x),s(y)) -> s(+(*(x,y),+(x,y)))
   *(*(x,y),z) -> *(x,*(y,z))
   sum(nil()) -> 0()
   sum(cons(x,l)) -> +(x,sum(l))
   prod(nil()) -> s(0())
   prod(cons(x,l)) -> *(x,prod(l))
  Open