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))
 app(nil(),l) -> l
 app(cons(x,l1),l2) -> cons(x,app(l1,l2))
 sum(nil()) -> 0()
 sum(cons(x,l)) -> +(x,sum(l))
 sum(app(l1,l2)) -> +(sum(l1),sum(l2))
 prod(nil()) -> s(0())
 prod(cons(x,l)) -> *(x,prod(l))
 prod(app(l1,l2)) -> *(prod(l1),prod(l2))

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))
   app#(cons(x,l1),l2) -> app#(l1,l2)
   sum#(cons(x,l)) -> sum#(l)
   sum#(cons(x,l)) -> +#(x,sum(l))
   sum#(app(l1,l2)) -> sum#(l2)
   sum#(app(l1,l2)) -> sum#(l1)
   sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
   prod#(cons(x,l)) -> prod#(l)
   prod#(cons(x,l)) -> *#(x,prod(l))
   prod#(app(l1,l2)) -> prod#(l2)
   prod#(app(l1,l2)) -> prod#(l1)
   prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
  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))
   app(nil(),l) -> l
   app(cons(x,l1),l2) -> cons(x,app(l1,l2))
   sum(nil()) -> 0()
   sum(cons(x,l)) -> +(x,sum(l))
   sum(app(l1,l2)) -> +(sum(l1),sum(l2))
   prod(nil()) -> s(0())
   prod(cons(x,l)) -> *(x,prod(l))
   prod(app(l1,l2)) -> *(prod(l1),prod(l2))
  Open