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

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

+'(x,_{1}x) -> +'(_{2}x,_{1}x)_{2}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 8

↳Dependency Graph

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Argument Filtering and Ordering

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

++'(x,_{1}x) -> ++'(_{2}x,_{1}x)_{2}

:(x,_{1}x) -> :(_{2}x,_{1}x)_{2}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 9

↳Dependency Graph

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳Argument Filtering and Ordering

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

-'(x,_{1}x) -> -'(_{2}x,_{1}x)_{2}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 10

↳Dependency Graph

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Argument Filtering and Ordering

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

LENGTH(x) -> LENGTH(_{1}x)_{1}

:(x,_{1}x) -> :(_{2}x,_{1}x)_{2}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 11

↳Dependency Graph

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳Argument Filtering and Ordering

→DP Problem 6

↳AFS

→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))

innermost

The following dependency pair can be strictly oriented:

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

The following usable rules for innermost can be oriented:

+(0,y) ->y

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

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

SUM(x) -> SUM(_{1}x)_{1}

:(x,_{1}x) -> :(_{2}x,_{1}x)_{2}

+(x,_{1}x) ->_{2}x_{2}

s(x) ->_{1}x_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 12

↳Dependency Graph

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳Argument Filtering and 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))

innermost

The following dependency pair can be strictly oriented:

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

The following usable rules for innermost can be oriented:

-(x, 0) ->x

-(0, s(y)) -> 0

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

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

QUOT(x,_{1}x) -> QUOT(_{2}x,_{1}x)_{2}

s(x) -> s(_{1}x)_{1}

-(x,_{1}x) ->_{2}x_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 5

↳AFS

→DP Problem 6

↳AFS

→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))

innermost

Duration:

0:01 minutes