YES
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))}
 DP:
  Strict:
   {                 +#(s(x), y) -> +#(x, y),
               ++#(:(x, xs), ys) -> ++#(xs, ys),
    sum#(++(xs, :(x, :(y, ys)))) -> ++#(xs, sum(:(x, :(y, ys)))),
    sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))),
    sum#(++(xs, :(x, :(y, ys)))) -> sum#(:(x, :(y, ys))),
            sum#(:(x, :(y, xs))) -> +#(x, y),
            sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)),
                  -#(s(x), s(y)) -> -#(x, y),
               quot#(s(x), s(y)) -> -#(x, y),
               quot#(s(x), s(y)) -> quot#(-(x, y), s(y)),
               length#(:(x, xs)) -> length#(xs),
                        avg#(xs) -> sum#(xs),
                        avg#(xs) -> quot#(hd(sum(xs)), length(xs)),
                        avg#(xs) -> length#(xs),
                        avg#(xs) -> hd#(sum(xs))}
  Weak:
  {                  +(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))}
  EDG:
   {(quot#(s(x), s(y)) -> quot#(-(x, y), s(y)), quot#(s(x), s(y)) -> quot#(-(x, y), s(y)))
    (quot#(s(x), s(y)) -> quot#(-(x, y), s(y)), quot#(s(x), s(y)) -> -#(x, y))
    (length#(:(x, xs)) -> length#(xs), length#(:(x, xs)) -> length#(xs))
    (avg#(xs) -> length#(xs), length#(:(x, xs)) -> length#(xs))
    (++#(:(x, xs), ys) -> ++#(xs, ys), ++#(:(x, xs), ys) -> ++#(xs, ys))
    (sum#(:(x, :(y, xs))) -> +#(x, y), +#(s(x), y) -> +#(x, y))
    (quot#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(:(x, :(y, ys))), sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(:(x, :(y, ys))), sum#(:(x, :(y, xs))) -> +#(x, y))
    (sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)), sum#(:(x, :(y, xs))) -> +#(x, y))
    (sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)), sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))), sum#(++(xs, :(x, :(y, ys)))) -> ++#(xs, sum(:(x, :(y, ys)))))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))), sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))), sum#(++(xs, :(x, :(y, ys)))) -> sum#(:(x, :(y, ys))))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))), sum#(:(x, :(y, xs))) -> +#(x, y))
    (sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))), sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
    (avg#(xs) -> sum#(xs), sum#(++(xs, :(x, :(y, ys)))) -> ++#(xs, sum(:(x, :(y, ys)))))
    (avg#(xs) -> sum#(xs), sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys))))))
    (avg#(xs) -> sum#(xs), sum#(++(xs, :(x, :(y, ys)))) -> sum#(:(x, :(y, ys))))
    (avg#(xs) -> sum#(xs), sum#(:(x, :(y, xs))) -> +#(x, y))
    (avg#(xs) -> sum#(xs), sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs)))
    (avg#(xs) -> quot#(hd(sum(xs)), length(xs)), quot#(s(x), s(y)) -> -#(x, y))
    (avg#(xs) -> quot#(hd(sum(xs)), length(xs)), quot#(s(x), s(y)) -> quot#(-(x, y), s(y)))
    (sum#(++(xs, :(x, :(y, ys)))) -> ++#(xs, sum(:(x, :(y, ys)))), ++#(:(x, xs), ys) -> ++#(xs, ys))}
   SCCS:
    Scc:
     {length#(:(x, xs)) -> length#(xs)}
    Scc:
     {quot#(s(x), s(y)) -> quot#(-(x, y), s(y))}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    Scc:
     {sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs))}
    Scc:
     {sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys)))))}
    Scc:
     {++#(:(x, xs), ys) -> ++#(xs, ys)}
    Scc:
     {+#(s(x), y) -> +#(x, y)}
    SCC:
     Strict:
      {length#(:(x, xs)) -> length#(xs)}
     Weak:
     {                  +(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))}
     SPSC:
      Simple Projection:
       pi(length#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {quot#(s(x), s(y)) -> quot#(-(x, y), s(y))}
     Weak:
     {                  +(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))}
     POLY:
      Argument Filtering:
       pi(avg) = [], pi(hd) = [], pi(length) = [], pi(quot#) = 0, pi(quot) = [], pi(-) = 0, pi(sum) = [], pi(:) = [], pi(nil) = [], pi(++) = [], pi(s) = [0], pi(0) = [], pi(+) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                  +(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))}
      Qed
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {                  +(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))}
     SPSC:
      Simple Projection:
       pi(-#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sum#(:(x, :(y, xs))) -> sum#(:(+(x, y), xs))}
     Weak:
     {                  +(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))}
     POLY:
      Argument Filtering:
       pi(avg) = [], pi(hd) = [], pi(length) = [], pi(quot) = [], pi(-) = [], pi(sum#) = 0, pi(sum) = [], pi(:) = [1], pi(nil) = [], pi(++) = [], pi(s) = [], pi(0) = [], pi(+) = []
      Usable Rules:
       {}
      Interpretation:
       [:](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                  +(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))}
      Qed
    SCC:
     Strict:
      {sum#(++(xs, :(x, :(y, ys)))) -> sum#(++(xs, sum(:(x, :(y, ys)))))}
     Weak:
     {                  +(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))}
     POLY:
      Argument Filtering:
       pi(avg) = [], pi(hd) = [], pi(length) = [], pi(quot) = [], pi(-) = [], pi(sum#) = 0, pi(sum) = [], pi(:) = [1], pi(nil) = [], pi(++) = [0,1], pi(s) = [], pi(0) = [], pi(+) = []
      Usable Rules:
       {}
      Interpretation:
       [:](x0) = x0 + 1,
       [++](x0, x1) = x0 + x1,
       [sum] = 1
      Strict:
       {}
      Weak:
       {                  +(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))}
      Qed
    SCC:
     Strict:
      {++#(:(x, xs), ys) -> ++#(xs, ys)}
     Weak:
     {                  +(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))}
     SPSC:
      Simple Projection:
       pi(++#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {+#(s(x), y) -> +#(x, y)}
     Weak:
     {                  +(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))}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {}
      Qed