MAYBE
Trs:
 {          0(#()) -> #(),
        sum(nil()) -> 0(#()),
   sum(cons(x, l)) -> +(x, sum(l)),
     +(0(x), 0(y)) -> 0(+(x, y)),
     +(0(x), 1(y)) -> 1(+(x, y)),
     +(+(x, y), z) -> +(x, +(y, z)),
         +(#(), x) -> x,
     +(1(x), 0(y)) -> 1(+(x, y)),
     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
         +(x, #()) -> x,
       prod(nil()) -> 1(#()),
  prod(cons(x, l)) -> *(x, prod(l)),
        *(0(x), y) -> 0(*(x, y)),
         *(#(), x) -> #(),
        *(1(x), y) -> +(0(*(x, y)), y),
     *(*(x, y), z) -> *(x, *(y, z))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open