(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) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LENGTH(:(x, xs)) → LENGTH(xs)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LENGTH(:(x, xs)) → LENGTH(xs)
The graph contains the following edges 1 > 1
(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) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
-1(s(x), s(y)) → -1(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- -1(s(x), s(y)) → -1(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(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: Polynomial interpretation [POLO]:
POL(-(x1, x2)) = x1
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(0, s(y)) → 0
(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) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
++1(:(x, xs), ys) → ++1(xs, ys)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- ++1(:(x, xs), ys) → ++1(xs, ys)
The graph contains the following edges 1 > 1, 2 >= 2
(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) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(s(x), y) → +1(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(28) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- +1(s(x), y) → +1(x, y)
The graph contains the following edges 1 > 1, 2 >= 2
(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) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(32) 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))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(34) 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))
The set Q consists of the following terms:
+(0, x0)
+(s(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
(35) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
The following rules are removed from R:
+(0, y) → y
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(+(x1, x2)) = x1 + x2
POL(0) = 0
POL(:(x1, x2)) = 2 + 2·x1 + 2·x2
POL(SUM(x1)) = 2·x1
POL(s(x1)) = x1
(36) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
+(s(x), y) → s(+(x, y))
The set Q consists of the following terms:
+(0, x0)
+(s(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
(37) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(38) TRUE
(39) 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.
(40) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(41) 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:
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
+(0, y) → y
+(s(x), y) → s(+(x, y))
sum(:(x, nil)) → :(x, nil)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(42) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
The following rules are removed from R:
++(nil, ys) → ys
+(0, y) → y
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(+(x1, x2)) = x1 + x2
POL(++(x1, x2)) = 2 + 2·x1 + x2
POL(0) = 0
POL(:(x1, x2)) = 2·x1 + x2
POL(SUM(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(sum(x1)) = x1
(43) 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:
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
++(:(x, xs), ys) → :(x, ++(xs, ys))
+(s(x), y) → s(+(x, y))
sum(:(x, nil)) → :(x, nil)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(44) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
Used ordering: Polynomial interpretation [POLO]:
POL(+(x1, x2)) = x1 + x2
POL(++(x1, x2)) = x1 + x2
POL(:(x1, x2)) = 1 + x1 + x2
POL(SUM(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(sum(x1)) = x1
(45) 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:
++(:(x, xs), ys) → :(x, ++(xs, ys))
+(s(x), y) → s(+(x, y))
sum(:(x, nil)) → :(x, nil)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(46) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(47) 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:
++(:(x, xs), ys) → :(x, ++(xs, ys))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(48) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
++(:(x, xs), ys) → :(x, ++(xs, ys))
Used ordering: Polynomial interpretation [POLO]:
POL(++(x1, x2)) = 2·x1 + 2·x2
POL(:(x1, x2)) = 2 + x1 + x2
POL(SUM(x1)) = 2·x1
POL(sum(x1)) = x1
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(50) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(51) TRUE