MAYBE
Trs:
 {              0(#()) -> #(),
            sum(nil()) -> 0(#()),
       sum(cons(x, l)) -> +(x, sum(l)),
      sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
         +(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,
         app(nil(), l) -> l,
  app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
           prod(nil()) -> 1(#()),
      prod(cons(x, l)) -> *(x, prod(l)),
     prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
            *(0(x), y) -> 0(*(x, y)),
             *(#(), x) -> #(),
            *(1(x), y) -> +(0(*(x, y)), y),
         *(*(x, y), z) -> *(x, *(y, z)),
         *(x, +(y, z)) -> +(*(x, y), *(x, z))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open