MAYBE
MAYBE
TRS:
 {
            0(#()) -> #(),
         +(x, #()) -> x,
         +(#(), x) -> x,
     +(0(x), 0(y)) -> 0(+(x, y)),
     +(0(x), 1(y)) -> 1(+(x, y)),
     +(+(x, y), z) -> +(x, +(y, z)),
     +(1(x), 0(y)) -> 1(+(x, y)),
     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
         *(#(), x) -> #(),
        *(0(x), y) -> 0(*(x, y)),
        *(1(x), y) -> +(0(*(x, y)), y),
     *(*(x, y), z) -> *(x, *(y, z)),
        sum(nil()) -> 0(#()),
   sum(cons(x, l)) -> +(x, sum(l)),
       prod(nil()) -> 1(#()),
  prod(cons(x, l)) -> *(x, prod(l))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
              0(#()) -> #(),
           +(x, #()) -> x,
           +(#(), x) -> x,
       +(0(x), 0(y)) -> 0(+(x, y)),
       +(0(x), 1(y)) -> 1(+(x, y)),
       +(+(x, y), z) -> +(x, +(y, z)),
       +(1(x), 0(y)) -> 1(+(x, y)),
       +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
           *(#(), x) -> #(),
          *(0(x), y) -> 0(*(x, y)),
          *(1(x), y) -> +(0(*(x, y)), y),
       *(*(x, y), z) -> *(x, *(y, z)),
          sum(nil()) -> 0(#()),
     sum(cons(x, l)) -> +(x, sum(l)),
         prod(nil()) -> 1(#()),
    prod(cons(x, l)) -> *(x, prod(l))
   }
  Fail