MAYBE
MAYBE
TRS:
 {
             +(x, 0()) -> x,
         +(+(x, y), z) -> +(x, +(y, z)),
             +(0(), x) -> x,
         +(s(x), s(y)) -> s(s(+(x, y))),
             *(x, 0()) -> 0(),
             *(0(), x) -> 0(),
         *(s(x), s(y)) -> s(+(*(x, y), +(x, 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()) -> s(0()),
      prod(cons(x, l)) -> *(x, prod(l))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
               +(x, 0()) -> x,
           +(+(x, y), z) -> +(x, +(y, z)),
               +(0(), x) -> x,
           +(s(x), s(y)) -> s(s(+(x, y))),
               *(x, 0()) -> 0(),
               *(0(), x) -> 0(),
           *(s(x), s(y)) -> s(+(*(x, y), +(x, 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()) -> s(0()),
        prod(cons(x, l)) -> *(x, prod(l))
   }
  Fail