MAYBE
MAYBE
TRS:
 {
                    +(0(), y) -> y,
                   +(s(x), y) -> s(+(x, y)),
                ++(nil(), ys) -> ys,
             ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
  sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))),
             sum(:(x, nil())) -> :(x, nil()),
          sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)),
                    -(x, 0()) -> x,
                 -(0(), s(y)) -> 0(),
                -(s(x), s(y)) -> -(x, y),
              quot(0(), s(y)) -> 0(),
             quot(s(x), s(y)) -> s(quot(-(x, y), s(y))),
                length(nil()) -> 0(),
             length(:(x, xs)) -> s(length(xs)),
                 hd(:(x, xs)) -> x,
                      avg(xs) -> quot(hd(sum(xs)), length(xs))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      +(0(), y) -> y,
                     +(s(x), y) -> s(+(x, y)),
                  ++(nil(), ys) -> ys,
               ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
    sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))),
               sum(:(x, nil())) -> :(x, nil()),
            sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)),
                      -(x, 0()) -> x,
                   -(0(), s(y)) -> 0(),
                  -(s(x), s(y)) -> -(x, y),
                quot(0(), s(y)) -> 0(),
               quot(s(x), s(y)) -> s(quot(-(x, y), s(y))),
                  length(nil()) -> 0(),
               length(:(x, xs)) -> s(length(xs)),
                   hd(:(x, xs)) -> x,
                        avg(xs) -> quot(hd(sum(xs)), length(xs))
   }
  Fail