MAYBE

Problem:
 0(#()) -> #()
 +(x,#()) -> x
 +(#(),x) -> x
 +(0(x),0(y)) -> 0(+(x,y))
 +(0(x),1(y)) -> 1(+(x,y))
 +(1(x),0(y)) -> 1(+(x,y))
 +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
 +(+(x,y),z) -> +(x,+(y,z))
 *(#(),x) -> #()
 *(0(x),y) -> 0(*(x,y))
 *(1(x),y) -> +(0(*(x,y)),y)
 *(*(x,y),z) -> *(x,*(y,z))
 *(x,+(y,z)) -> +(*(x,y),*(x,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()) -> 1(#())
 prod(cons(x,l)) -> *(x,prod(l))
 prod(app(l1,l2)) -> *(prod(l1),prod(l2))

Proof:
 DP Processor:
  DPs:
   +#(0(x),0(y)) -> +#(x,y)
   +#(0(x),0(y)) -> 0#(+(x,y))
   +#(0(x),1(y)) -> +#(x,y)
   +#(1(x),0(y)) -> +#(x,y)
   +#(1(x),1(y)) -> +#(x,y)
   +#(1(x),1(y)) -> +#(+(x,y),1(#()))
   +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   *#(0(x),y) -> *#(x,y)
   *#(0(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> *#(x,y)
   *#(1(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> +#(0(*(x,y)),y)
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
   *#(x,+(y,z)) -> *#(x,z)
   *#(x,+(y,z)) -> *#(x,y)
   *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
   app#(cons(x,l1),l2) -> app#(l1,l2)
   sum#(nil()) -> 0#(#())
   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:
   0(#()) -> #()
   +(x,#()) -> x
   +(#(),x) -> x
   +(0(x),0(y)) -> 0(+(x,y))
   +(0(x),1(y)) -> 1(+(x,y))
   +(1(x),0(y)) -> 1(+(x,y))
   +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
   +(+(x,y),z) -> +(x,+(y,z))
   *(#(),x) -> #()
   *(0(x),y) -> 0(*(x,y))
   *(1(x),y) -> +(0(*(x,y)),y)
   *(*(x,y),z) -> *(x,*(y,z))
   *(x,+(y,z)) -> +(*(x,y),*(x,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()) -> 1(#())
   prod(cons(x,l)) -> *(x,prod(l))
   prod(app(l1,l2)) -> *(prod(l1),prod(l2))
  Usable Rule Processor:
   DPs:
    +#(0(x),0(y)) -> +#(x,y)
    +#(0(x),0(y)) -> 0#(+(x,y))
    +#(0(x),1(y)) -> +#(x,y)
    +#(1(x),0(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(+(x,y),1(#()))
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    *#(0(x),y) -> *#(x,y)
    *#(0(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> *#(x,y)
    *#(1(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> +#(0(*(x,y)),y)
    *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z))
    *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    app#(cons(x,l1),l2) -> app#(l1,l2)
    sum#(nil()) -> 0#(#())
    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,#()) -> x
    +(#(),x) -> x
    +(0(x),0(y)) -> 0(+(x,y))
    +(0(x),1(y)) -> 1(+(x,y))
    +(1(x),0(y)) -> 1(+(x,y))
    +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
    +(+(x,y),z) -> +(x,+(y,z))
    0(#()) -> #()
    *(#(),x) -> #()
    *(0(x),y) -> 0(*(x,y))
    *(1(x),y) -> +(0(*(x,y)),y)
    *(*(x,y),z) -> *(x,*(y,z))
    *(x,+(y,z)) -> +(*(x,y),*(x,z))
    sum(nil()) -> 0(#())
    sum(cons(x,l)) -> +(x,sum(l))
    sum(app(l1,l2)) -> +(sum(l1),sum(l2))
    prod(nil()) -> 1(#())
    prod(cons(x,l)) -> *(x,prod(l))
    prod(app(l1,l2)) -> *(prod(l1),prod(l2))
   Open