Consider the TRS R consisting of the rewrite rules

1: 0 + y -> y
2: s(x) + y -> s(x + y)
3: nil ++ ys -> ys
4: (x : xs) ++ ys -> x : (xs ++ ys)
5: sum(x : nil) -> x : nil
6: sum(x : (y : xs)) -> sum((x + y) : xs)
7: sum(xs ++ (x : (y : ys))) -> sum(xs ++ sum(x : (y : ys)))
8: x - 0 -> x
9: 0 - s(y) -> 0
10: s(x) - s(y) -> x - y
11: quot(0,s(y)) -> 0
12: quot(s(x),s(y)) -> s(quot(x - y,s(y)))
13: length(nil) -> 0
14: length(x : xs) -> s(length(xs))
15: hd(x : xs) -> x
16: avg(xs) -> quot(hd(sum(xs)),length(xs))

There are 15 dependency pairs:

17: s(x) +# y -> x +# y
18: (x : xs) ++# ys -> xs ++# ys
19: SUM(x : (y : xs)) -> SUM((x + y) : xs)
20: SUM(x : (y : xs)) -> x +# y
21: SUM(xs ++ (x : (y : ys))) -> SUM(xs ++ sum(x : (y : ys)))
22: SUM(xs ++ (x : (y : ys))) -> xs ++# sum(x : (y : ys))
23: SUM(xs ++ (x : (y : ys))) -> SUM(x : (y : ys))
24: s(x) -# s(y) -> x -# y
25: QUOT(s(x),s(y)) -> QUOT(x - y,s(y))
26: QUOT(s(x),s(y)) -> x -# y
27: LENGTH(x : xs) -> LENGTH(xs)
28: AVG(xs) -> QUOT(hd(sum(xs)),length(xs))
29: AVG(xs) -> HD(sum(xs))
30: AVG(xs) -> SUM(xs)
31: AVG(xs) -> LENGTH(xs)

The approximated dependency graph contains 7 SCCs:
{17},
{18},
{24},
{27},
{25},
{19}
and {21}.

- Consider the SCC {17}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [+#](x,y) = x + y + 1,
rule 17
is strictly decreasing.

- Consider the SCC {18}.
There are no usable rules.
By taking the polynomial interpretation
[++#](x,y) = [:](x,y) = x + y + 1,
rule 18
is strictly decreasing.

- Consider the SCC {24}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [-#](x,y) = x + y + 1,
rule 24
is strictly decreasing.

- Consider the SCC {27}.
There are no usable rules.
By taking the polynomial interpretation
[LENGTH](x) = x + 1
and [:](x,y) = x + y + 1,
rule 27
is strictly decreasing.

- Consider the SCC {25}.
The usable rules are {8-10}.
By taking the polynomial interpretation
[0] = 1,
[-](x,y) = x,
[s](x) = x + 1
and [QUOT](x,y) = x + y + 1,
the rules in {8,9}
are weakly decreasing and
the rules in {10,25}
are strictly decreasing.

- Consider the SCC {19}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = 1,
[s](x) = [SUM](x) = x + 1,
[+](x,y) = x + y + 1
and [:](x,y) = y + 1,
rule 2
is weakly decreasing and
the rules in {1,19}
are strictly decreasing.

- Consider the SCC {21}.
The usable rules are {1-7}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [sum](x) = 1,
[s](x) = [SUM](x) = x + 1,
[+](x,y) = [++](x,y) = x + y + 1
and [:](x,y) = y + 1,
the rules in {2,4-7}
are weakly decreasing and
the rules in {1,3,21}
are strictly decreasing.

Hence the TRS is terminating.