+(0,

+(s(

++(nil,

++(:(

sum(:(

sum(:(

sum(++(

-(

-(0, s(

-(s(

quot(0, s(

quot(s(

length(nil) -> 0

length(:(

hd(:(

avg(

R

↳Dependency Pair Analysis

+'(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

↳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*))

Duration:

0:02 minutes