Term Rewriting System R:
[y, x, ys, xs]
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

+'(s(x), y) -> +'(x, y)
++'(:(x, xs), ys) -> ++'(xs, ys)
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
SUM(:(x, :(y, xs))) -> +'(x, y)
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(:(x, :(y, ys)))
-'(s(x), s(y)) -> -'(x, y)
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
QUOT(s(x), s(y)) -> -'(x, y)
LENGTH(:(x, xs)) -> LENGTH(xs)
AVG(xs) -> QUOT(hd(sum(xs)), length(xs))
AVG(xs) -> HD(sum(xs))
AVG(xs) -> SUM(xs)
AVG(xs) -> LENGTH(xs)

Furthermore, R contains seven SCCs.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Remaining Obligation(s)`
`       →DP Problem 2`
`         ↳Remaining Obligation(s)`
`       →DP Problem 3`
`         ↳Remaining Obligation(s)`
`       →DP Problem 4`
`         ↳Remaining Obligation(s)`
`       →DP Problem 5`
`         ↳Remaining Obligation(s)`
`       →DP Problem 6`
`         ↳Remaining Obligation(s)`
`       →DP Problem 7`
`         ↳Remaining Obligation(s)`

The following remains to be proven:
• Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

• Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(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))

Termination of R could not be shown.
Duration:
0:02 minutes