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

↳Polynomial Ordering

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

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

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(length(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(+'(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 8

↳Dependency Graph

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polynomial Ordering

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

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

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(++'(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(length(x)_{1})= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 9

↳Dependency Graph

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polynomial Ordering

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

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

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(-'(x)_{1}, x_{2})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(length(x)_{1})= x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 10

↳Dependency Graph

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polynomial Ordering

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

**LENGTH(:( x, xs)) -> LENGTH(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))

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(LENGTH(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(length(x)_{1})= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 11

↳Dependency Graph

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polynomial Ordering

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

**SUM(:( x, :(y, xs))) -> SUM(:(+(x, y), 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))

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(SUM(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(length(x)_{1})= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 12

↳Dependency Graph

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polynomial Ordering

→DP Problem 7

↳Remaining

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

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

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(sum(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(-(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(avg(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(QUOT(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(hd(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(++(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(quot(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(+(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(length(x)_{1})= x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 13

↳Dependency Graph

→DP Problem 7

↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 4

↳Polo

→DP Problem 5

↳Polo

→DP Problem 6

↳Polo

→DP Problem 7

↳Remaining Obligation(s)

The following remains to be proven:

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

+(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:00 minutes