MAYBE
Trs:
 {                  +(0(), y) -> y,
                   +(s(x), y) -> s(+(x, y)),
                ++(nil(), ys) -> ys,
             ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
                 -(0(), s(y)) -> 0(),
                -(s(x), s(y)) -> -(x, y),
                    -(x, 0()) -> x,
                      avg(xs) -> quot(hd(sum(xs)), length(xs)),
                length(nil()) -> 0(),
             length(:(x, xs)) -> s(length(xs)),
  sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))),
             sum(:(x, nil())) -> :(x, nil()),
          sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)),
                 hd(:(x, xs)) -> x,
              quot(0(), s(y)) -> 0(),
             quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open