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