(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(s(x), y) → +1(x, y)
++1(:(x, xs), ys) → ++1(xs, ys)
SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
SUM(:(x, :(y, xs))) → +1(x, y)
SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))
SUM(++(xs, :(x, :(y, ys)))) → ++1(xs, sum(:(x, :(y, ys))))
SUM(++(xs, :(x, :(y, ys)))) → SUM(:(x, :(y, ys)))
-1(s(x), s(y)) → -1(x, y)
QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
QUOT(s(x), s(y)) → -1(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)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 8 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(:(x, xs)) → LENGTH(xs)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


LENGTH(:(x, xs)) → LENGTH(xs)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LENGTH(x1)  =  LENGTH(x1)
:(x1, x2)  =  :(x1, x2)
+(x1, x2)  =  x2
0  =  0
s(x1)  =  x1
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
sum(x1)  =  x1
-(x1, x2)  =  -(x1, x2)
quot(x1, x2)  =  quot
length(x1)  =  length
hd(x1)  =  hd(x1)
avg(x1)  =  avg

Recursive path order with status [RPO].
Quasi-Precedence:
[0, -2, quot, length, hd1, avg]
++2 > [:2, nil]

Status:
LENGTH1: [1]
:2: multiset
0: multiset
++2: [2,1]
nil: multiset
-2: multiset
quot: multiset
length: multiset
hd1: multiset
avg: multiset


The following usable rules [FROCOS05] were 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))

(7) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(9) TRUE

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-1(s(x), s(y)) → -1(x, y)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


-1(s(x), s(y)) → -1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
-1(x1, x2)  =  -1(x2)
s(x1)  =  s(x1)
+(x1, x2)  =  +(x1, x2)
0  =  0
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
:(x1, x2)  =  :(x1, x2)
sum(x1)  =  x1
-(x1, x2)  =  x1
quot(x1, x2)  =  quot(x1)
length(x1)  =  length(x1)
hd(x1)  =  hd(x1)
avg(x1)  =  avg(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
++2 > :2 > +2 > [-^11, s1, nil]
[length1, avg1] > [0, quot1] > [-^11, s1, nil]
[length1, avg1] > hd1 > [-^11, s1, nil]

Status:
-^11: multiset
s1: [1]
+2: [2,1]
0: multiset
++2: [2,1]
nil: multiset
:2: [2,1]
quot1: multiset
length1: [1]
hd1: multiset
avg1: multiset


The following usable rules [FROCOS05] were 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))

(12) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(14) TRUE

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
QUOT(x1, x2)  =  QUOT(x1, x2)
s(x1)  =  s(x1)
-(x1, x2)  =  x1
+(x1, x2)  =  +(x1, x2)
0  =  0
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
:(x1, x2)  =  :(x1, x2)
sum(x1)  =  x1
quot(x1, x2)  =  quot(x1, x2)
length(x1)  =  length(x1)
hd(x1)  =  x1
avg(x1)  =  avg(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
++2 > [+2, :2] > [QUOT2, s1]
avg1 > [0, nil, length1] > [QUOT2, s1]
avg1 > quot2 > [QUOT2, s1]

Status:
QUOT2: multiset
s1: multiset
+2: [2,1]
0: multiset
++2: [2,1]
nil: multiset
:2: [2,1]
quot2: [1,2]
length1: multiset
avg1: multiset


The following usable rules [FROCOS05] were 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))

(17) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(19) TRUE

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

++1(:(x, xs), ys) → ++1(xs, ys)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


++1(:(x, xs), ys) → ++1(xs, ys)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
++1(x1, x2)  =  ++1(x1, x2)
:(x1, x2)  =  :(x1, x2)
+(x1, x2)  =  x2
0  =  0
s(x1)  =  x1
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
sum(x1)  =  x1
-(x1, x2)  =  -(x1)
quot(x1, x2)  =  x2
length(x1)  =  length(x1)
hd(x1)  =  hd(x1)
avg(x1)  =  avg(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
++2 > [++^12, :2] > nil > [0, length1, avg1]
-1 > [0, length1, avg1]
hd1 > [0, length1, avg1]

Status:
++^12: [2,1]
:2: multiset
0: multiset
++2: [1,2]
nil: multiset
-1: multiset
length1: multiset
hd1: [1]
avg1: multiset


The following usable rules [FROCOS05] were 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))

(22) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(24) TRUE

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+1(s(x), y) → +1(x, y)

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


+1(s(x), y) → +1(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
+1(x1, x2)  =  +1(x1, x2)
s(x1)  =  s(x1)
+(x1, x2)  =  +(x1, x2)
0  =  0
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
:(x1, x2)  =  :(x1, x2)
sum(x1)  =  x1
-(x1, x2)  =  x1
quot(x1, x2)  =  x1
length(x1)  =  length(x1)
hd(x1)  =  hd(x1)
avg(x1)  =  avg(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
++2 > [+2, :2] > s1
++2 > [+2, :2] > nil
[length1, avg1] > s1
[length1, avg1] > 0
[length1, avg1] > hd1

Status:
+^12: [2,1]
s1: multiset
+2: [2,1]
0: multiset
++2: multiset
nil: multiset
:2: [2,1]
length1: multiset
hd1: multiset
avg1: multiset


The following usable rules [FROCOS05] were 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))

(27) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) TRUE

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SUM(x1)  =  x1
:(x1, x2)  =  :(x1, x2)
+(x1, x2)  =  +(x1, x2)
0  =  0
s(x1)  =  x1
++(x1, x2)  =  ++(x1, x2)
nil  =  nil
sum(x1)  =  x1
-(x1, x2)  =  -(x1, x2)
quot(x1, x2)  =  quot
length(x1)  =  length
hd(x1)  =  hd(x1)
avg(x1)  =  avg

Recursive path order with status [RPO].
Quasi-Precedence:
++2 > :2 > +2
nil > 0
-2 > 0
[quot, avg] > 0
length > 0

Status:
:2: [2,1]
+2: multiset
0: multiset
++2: [2,1]
nil: multiset
-2: multiset
quot: multiset
length: multiset
hd1: multiset
avg: multiset


The following usable rules [FROCOS05] were 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))

(32) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(34) TRUE

(35) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))

The TRS R consists of the following 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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.