YES(O(1), O(n^2)) 61.81/22.04 YES(O(1), O(n^2)) 61.81/22.06 61.81/22.06 61.81/22.06 61.81/22.06 61.81/22.06 61.81/22.06 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 61.81/22.06 61.81/22.06 61.81/22.06
61.81/22.06
61.81/22.06
61.81/22.06
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS
61.81/22.06 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳2 CdtProblem
61.81/22.06 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳4 CdtProblem
61.81/22.06 
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳6 CdtProblem
61.81/22.06 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
61.81/22.06 
↳8 CdtProblem
61.81/22.06 
↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳10 CdtProblem
61.81/22.06 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
61.81/22.06 
↳12 CdtProblem
61.81/22.06 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
61.81/22.06 
↳14 CdtProblem
61.81/22.06 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
61.81/22.06 
↳16 CdtProblem
61.81/22.06 
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
61.81/22.06 
↳18 CdtProblem
61.81/22.06 
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
61.81/22.06 
↳20 CdtProblem
61.81/22.06 
↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳22 CdtProblem
61.81/22.06 
↳23 CdtUnreachableProof (⇔)
61.81/22.06 
↳24 CdtProblem
61.81/22.06 
↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
61.81/22.06 
↳26 CdtProblem
61.81/22.06 
↳27 SIsEmptyProof (BOTH BOUNDS(ID, ID))
61.81/22.06 
↳28 BOUNDS(O(1), O(1))
61.81/22.06
61.81/22.06 61.81/22.06
61.81/22.06
61.81/22.06

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

+(0, y) → y 61.81/22.06
+(s(x), y) → s(+(x, y)) 61.81/22.06
++(nil, ys) → ys 61.81/22.06
++(:(x, xs), ys) → :(x, ++(xs, ys)) 61.81/22.06
sum(:(x, nil)) → :(x, nil) 61.81/22.06
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs)) 61.81/22.06
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys))))) 61.81/22.06
-(x, 0) → x 61.81/22.06
-(0, s(y)) → 0 61.81/22.06
-(s(x), s(y)) → -(x, y) 61.81/22.06
quot(0, s(y)) → 0 61.81/22.06
quot(s(x), s(y)) → s(quot(-(x, y), s(y))) 61.81/22.06
length(nil) → 0 61.81/22.06
length(:(x, xs)) → s(length(xs)) 61.81/22.06
hd(:(x, xs)) → x 61.81/22.06
avg(xs) → quot(hd(sum(xs)), length(xs))

Rewrite Strategy: INNERMOST
61.81/22.06
61.81/22.06

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
61.81/22.06
61.81/22.06

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.06
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.06
++(nil, z0) → z0 61.81/22.06
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.06
sum(:(z0, nil)) → :(z0, nil) 61.81/22.06
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.06
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.06
-(z0, 0) → z0 61.81/22.06
-(0, s(z0)) → 0 61.81/22.06
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.06
quot(0, s(z0)) → 0 61.81/22.06
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.06
length(nil) → 0 61.81/22.06
length(:(z0, z1)) → s(length(z1)) 61.81/22.06
hd(:(z0, z1)) → z0 61.81/22.06
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.06
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.06
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.06
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.06
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.06
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.06
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.06
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.06
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.06
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.06
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.06
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.06
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.06
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.06
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c15

61.81/22.06
61.81/22.06

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
61.81/22.06
61.81/22.06

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.06
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.06
++(nil, z0) → z0 61.81/22.06
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.06
sum(:(z0, nil)) → :(z0, nil) 61.81/22.06
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.06
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.06
-(z0, 0) → z0 61.81/22.06
-(0, s(z0)) → 0 61.81/22.06
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.09
quot(0, s(z0)) → 0 61.81/22.09
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), SUM(z0), LENGTH(z0))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), SUM(z0), LENGTH(z0))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c15

61.81/22.09
61.81/22.09

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC
61.81/22.09
61.81/22.09

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.09
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.09
++(nil, z0) → z0 61.81/22.09
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.09
sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.09
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.09
-(z0, 0) → z0 61.81/22.09
-(0, s(z0)) → 0 61.81/22.09
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.09
quot(0, s(z0)) → 0 61.81/22.09
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 61.81/22.09
AVG(z0) → c(SUM(z0)) 61.81/22.09
AVG(z0) → c(LENGTH(z0))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 61.81/22.09
AVG(z0) → c(SUM(z0)) 61.81/22.09
AVG(z0) → c(LENGTH(z0))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

61.81/22.09
61.81/22.09

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

AVG(z0) → c(SUM(z0)) 61.81/22.09
AVG(z0) → c(LENGTH(z0))
61.81/22.09
61.81/22.09

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.09
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.09
++(nil, z0) → z0 61.81/22.09
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.09
sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.09
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.09
-(z0, 0) → z0 61.81/22.09
-(0, s(z0)) → 0 61.81/22.09
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.09
quot(0, s(z0)) → 0 61.81/22.09
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

61.81/22.09
61.81/22.09

(9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
61.81/22.09
61.81/22.09

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.09
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.09
++(nil, z0) → z0 61.81/22.09
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.09
sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.09
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.09
-(z0, 0) → z0 61.81/22.09
-(0, s(z0)) → 0 61.81/22.09
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.09
quot(0, s(z0)) → 0 61.81/22.09
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

61.81/22.09
61.81/22.09

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.09
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
+(0, z0) → z0 61.81/22.09
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.09
-(z0, 0) → z0 61.81/22.09
-(0, s(z0)) → 0 61.81/22.09
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 61.81/22.09

POL(+(x1, x2)) = 0    61.81/22.09
POL(+'(x1, x2)) = [2]    61.81/22.09
POL(++(x1, x2)) = [4]x2    61.81/22.09
POL(++'(x1, x2)) = [1]    61.81/22.09
POL(-(x1, x2)) = 0    61.81/22.09
POL(-'(x1, x2)) = 0    61.81/22.09
POL(0) = 0    61.81/22.09
POL(:(x1, x2)) = [3] + x2    61.81/22.09
POL(AVG(x1)) = [5] + [5]x1    61.81/22.09
POL(LENGTH(x1)) = 0    61.81/22.09
POL(QUOT(x1, x2)) = [1]    61.81/22.09
POL(SUM(x1)) = [4]x1    61.81/22.09
POL(c(x1)) = x1    61.81/22.09
POL(c1(x1)) = x1    61.81/22.09
POL(c11(x1, x2)) = x1 + x2    61.81/22.09
POL(c13(x1)) = x1    61.81/22.09
POL(c3(x1)) = x1    61.81/22.09
POL(c5(x1, x2)) = x1 + x2    61.81/22.09
POL(c6(x1, x2, x3)) = x1 + x2 + x3    61.81/22.09
POL(c9(x1)) = x1    61.81/22.09
POL(hd(x1)) = [1]    61.81/22.09
POL(length(x1)) = [4] + [2]x1    61.81/22.09
POL(nil) = 0    61.81/22.09
POL(s(x1)) = x1    61.81/22.09
POL(sum(x1)) = [3]   
61.81/22.09
61.81/22.09

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.09
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.09
++(nil, z0) → z0 61.81/22.09
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.09
sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.09
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.09
-(z0, 0) → z0 61.81/22.09
-(0, s(z0)) → 0 61.81/22.09
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.09
quot(0, s(z0)) → 0 61.81/22.09
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.09
length(nil) → 0 61.81/22.09
length(:(z0, z1)) → s(length(z1)) 61.81/22.09
hd(:(z0, z1)) → z0 61.81/22.09
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.09
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.09
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.09
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.09
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.09
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 61.81/22.09
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.09
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

61.81/22.09
61.81/22.09

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LENGTH(:(z0, z1)) → c13(LENGTH(z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 61.81/22.09
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.10
hd(:(z0, z1)) → z0 61.81/22.10
length(nil) → 0 61.81/22.10
length(:(z0, z1)) → s(length(z1)) 61.81/22.10
+(0, z0) → z0 61.81/22.10
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.10
-(z0, 0) → z0 61.81/22.10
-(0, s(z0)) → 0 61.81/22.10
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 61.81/22.10

POL(+(x1, x2)) = 0    61.81/22.10
POL(+'(x1, x2)) = 0    61.81/22.10
POL(++(x1, x2)) = 0    61.81/22.10
POL(++'(x1, x2)) = 0    61.81/22.10
POL(-(x1, x2)) = 0    61.81/22.10
POL(-'(x1, x2)) = 0    61.81/22.10
POL(0) = 0    61.81/22.10
POL(:(x1, x2)) = [2] + x2    61.81/22.10
POL(AVG(x1)) = [5] + [5]x1    61.81/22.10
POL(LENGTH(x1)) = [2]x1    61.81/22.10
POL(QUOT(x1, x2)) = 0    61.81/22.10
POL(SUM(x1)) = 0    61.81/22.10
POL(c(x1)) = x1    61.81/22.10
POL(c1(x1)) = x1    61.81/22.10
POL(c11(x1, x2)) = x1 + x2    61.81/22.10
POL(c13(x1)) = x1    61.81/22.10
POL(c3(x1)) = x1    61.81/22.10
POL(c5(x1, x2)) = x1 + x2    61.81/22.10
POL(c6(x1, x2, x3)) = x1 + x2 + x3    61.81/22.10
POL(c9(x1)) = x1    61.81/22.10
POL(hd(x1)) = [1]    61.81/22.10
POL(length(x1)) = [4] + [3]x1    61.81/22.10
POL(nil) = 0    61.81/22.10
POL(s(x1)) = x1    61.81/22.10
POL(sum(x1)) = [4]   
61.81/22.10
61.81/22.10

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.10
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.10
++(nil, z0) → z0 61.81/22.10
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.10
sum(:(z0, nil)) → :(z0, nil) 61.81/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.10
-(z0, 0) → z0 61.81/22.10
-(0, s(z0)) → 0 61.81/22.10
-(s(z0), s(z1)) → -(z0, z1) 61.81/22.10
quot(0, s(z0)) → 0 61.81/22.10
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 61.81/22.10
length(nil) → 0 61.81/22.10
length(:(z0, z1)) → s(length(z1)) 61.81/22.10
hd(:(z0, z1)) → z0 61.81/22.10
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 61.81/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

61.81/22.10
61.81/22.10

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 61.81/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 61.81/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 61.81/22.10
hd(:(z0, z1)) → z0 61.81/22.10
length(nil) → 0 61.81/22.10
length(:(z0, z1)) → s(length(z1)) 61.81/22.10
+(0, z0) → z0 61.81/22.10
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.10
-(z0, 0) → z0 61.81/22.10
-(0, s(z0)) → 0 61.81/22.10
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 61.81/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 61.81/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 61.81/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 61.81/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 61.81/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 61.81/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 61.81/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 61.81/22.10

POL(+(x1, x2)) = [2] + x1 + x2    61.81/22.10
POL(+'(x1, x2)) = 0    61.81/22.10
POL(++(x1, x2)) = 0    61.81/22.10
POL(++'(x1, x2)) = 0    61.81/22.10
POL(-(x1, x2)) = x1    61.81/22.10
POL(-'(x1, x2)) = [1]    61.81/22.10
POL(0) = 0    61.81/22.10
POL(:(x1, x2)) = [4] + x1 + x2    61.81/22.10
POL(AVG(x1)) = [5] + [5]x1    61.81/22.10
POL(LENGTH(x1)) = [5]x1    61.81/22.10
POL(QUOT(x1, x2)) = [1] + x1    61.81/22.10
POL(SUM(x1)) = 0    61.81/22.10
POL(c(x1)) = x1    61.81/22.10
POL(c1(x1)) = x1    61.81/22.10
POL(c11(x1, x2)) = x1 + x2    61.81/22.10
POL(c13(x1)) = x1    61.81/22.10
POL(c3(x1)) = x1    61.81/22.10
POL(c5(x1, x2)) = x1 + x2    61.81/22.10
POL(c6(x1, x2, x3)) = x1 + x2 + x3    61.81/22.10
POL(c9(x1)) = x1    61.81/22.10
POL(hd(x1)) = [2] + x1    61.81/22.10
POL(length(x1)) = 0    61.81/22.10
POL(nil) = 0    61.81/22.10
POL(s(x1)) = [4] + x1    61.81/22.10
POL(sum(x1)) = [2] + [4]x1   
61.81/22.10
61.81/22.10

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 61.81/22.10
+(s(z0), z1) → s(+(z0, z1)) 61.81/22.10
++(nil, z0) → z0 61.81/22.10
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 61.81/22.10
sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.10
quot(0, s(z0)) → 0 62.12/22.10
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

62.12/22.10
62.12/22.10

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

++'(:(z0, z1), z2) → c3(++'(z1, z2))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
+(0, z0) → z0 62.12/22.10
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 62.12/22.10

POL(+(x1, x2)) = 0    62.12/22.10
POL(+'(x1, x2)) = 0    62.12/22.10
POL(++(x1, x2)) = x2 + x22 + x1·x2    62.12/22.10
POL(++'(x1, x2)) = x1    62.12/22.10
POL(-(x1, x2)) = 0    62.12/22.10
POL(-'(x1, x2)) = 0    62.12/22.10
POL(0) = 0    62.12/22.10
POL(:(x1, x2)) = [1] + x2    62.12/22.10
POL(AVG(x1)) = [3]x1 + x12    62.12/22.10
POL(LENGTH(x1)) = [3]x1 + [3]x12    62.12/22.10
POL(QUOT(x1, x2)) = 0    62.12/22.10
POL(SUM(x1)) = x1    62.12/22.10
POL(c(x1)) = x1    62.12/22.10
POL(c1(x1)) = x1    62.12/22.10
POL(c11(x1, x2)) = x1 + x2    62.12/22.10
POL(c13(x1)) = x1    62.12/22.10
POL(c3(x1)) = x1    62.12/22.10
POL(c5(x1, x2)) = x1 + x2    62.12/22.10
POL(c6(x1, x2, x3)) = x1 + x2 + x3    62.12/22.10
POL(c9(x1)) = x1    62.12/22.10
POL(hd(x1)) = 0    62.12/22.10
POL(length(x1)) = 0    62.12/22.10
POL(nil) = 0    62.12/22.10
POL(s(x1)) = 0    62.12/22.10
POL(sum(x1)) = [1]   
62.12/22.10
62.12/22.10

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 62.12/22.10
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.10
++(nil, z0) → z0 62.12/22.10
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 62.12/22.10
sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.10
quot(0, s(z0)) → 0 62.12/22.10
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

62.12/22.10
62.12/22.10

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

-'(s(z0), s(z1)) → c9(-'(z0, z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
+(0, z0) → z0 62.12/22.10
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 62.12/22.10

POL(+(x1, x2)) = x1 + x2    62.12/22.10
POL(+'(x1, x2)) = 0    62.12/22.10
POL(++(x1, x2)) = 0    62.12/22.10
POL(++'(x1, x2)) = 0    62.12/22.10
POL(-(x1, x2)) = x1    62.12/22.10
POL(-'(x1, x2)) = [2]x1    62.12/22.10
POL(0) = 0    62.12/22.10
POL(:(x1, x2)) = x1 + x2    62.12/22.10
POL(AVG(x1)) = x12    62.12/22.10
POL(LENGTH(x1)) = [3]x1 + [3]x12    62.12/22.10
POL(QUOT(x1, x2)) = x12    62.12/22.10
POL(SUM(x1)) = 0    62.12/22.10
POL(c(x1)) = x1    62.12/22.10
POL(c1(x1)) = x1    62.12/22.10
POL(c11(x1, x2)) = x1 + x2    62.12/22.10
POL(c13(x1)) = x1    62.12/22.10
POL(c3(x1)) = x1    62.12/22.10
POL(c5(x1, x2)) = x1 + x2    62.12/22.10
POL(c6(x1, x2, x3)) = x1 + x2 + x3    62.12/22.10
POL(c9(x1)) = x1    62.12/22.10
POL(hd(x1)) = x1    62.12/22.10
POL(length(x1)) = 0    62.12/22.10
POL(nil) = 0    62.12/22.10
POL(s(x1)) = [1] + x1    62.12/22.10
POL(sum(x1)) = x1   
62.12/22.10
62.12/22.10

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 62.12/22.10
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.10
++(nil, z0) → z0 62.12/22.10
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 62.12/22.10
sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.10
quot(0, s(z0)) → 0 62.12/22.10
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

62.12/22.10
62.12/22.10

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) by

SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2)))) 62.12/22.10
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
62.12/22.10
62.12/22.10

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 62.12/22.10
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.10
++(nil, z0) → z0 62.12/22.10
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 62.12/22.10
sum(:(z0, nil)) → :(z0, nil) 62.12/22.10
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.10
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.10
-(z0, 0) → z0 62.12/22.10
-(0, s(z0)) → 0 62.12/22.10
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.10
quot(0, s(z0)) → 0 62.12/22.10
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.10
length(nil) → 0 62.12/22.10
length(:(z0, z1)) → s(length(z1)) 62.12/22.10
hd(:(z0, z1)) → z0 62.12/22.10
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.10
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.10
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.10
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.10
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.10
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.10
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.11
SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2)))) 62.12/22.11
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c9, c11, c13, c, c6, c6

62.12/22.11
62.12/22.11

(23) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2)))) 62.12/22.11
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
62.12/22.11
62.12/22.11

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 62.12/22.11
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.11
++(nil, z0) → z0 62.12/22.11
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 62.12/22.11
sum(:(z0, nil)) → :(z0, nil) 62.12/22.11
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.11
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.11
-(z0, 0) → z0 62.12/22.11
-(0, s(z0)) → 0 62.12/22.11
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.11
quot(0, s(z0)) → 0 62.12/22.11
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.11
length(nil) → 0 62.12/22.11
length(:(z0, z1)) → s(length(z1)) 62.12/22.11
hd(:(z0, z1)) → z0 62.12/22.11
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c9, c11, c13, c

62.12/22.11
62.12/22.11

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(s(z0), z1) → c1(+'(z0, z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil) 62.12/22.11
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.11
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.11
hd(:(z0, z1)) → z0 62.12/22.11
length(nil) → 0 62.12/22.11
length(:(z0, z1)) → s(length(z1)) 62.12/22.11
+(0, z0) → z0 62.12/22.11
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.11
-(z0, 0) → z0 62.12/22.11
-(0, s(z0)) → 0 62.12/22.11
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 62.12/22.11

POL(+(x1, x2)) = x1 + x2    62.12/22.11
POL(+'(x1, x2)) = x1 + [2]x2    62.12/22.11
POL(++(x1, x2)) = [3]x22    62.12/22.11
POL(++'(x1, x2)) = [3]x1 + [3]x1·x2 + [3]x12    62.12/22.11
POL(-(x1, x2)) = 0    62.12/22.11
POL(-'(x1, x2)) = 0    62.12/22.11
POL(0) = 0    62.12/22.11
POL(:(x1, x2)) = [1] + x1 + x2    62.12/22.11
POL(AVG(x1)) = [3]    62.12/22.11
POL(LENGTH(x1)) = [3]x1 + [3]x12    62.12/22.11
POL(QUOT(x1, x2)) = 0    62.12/22.11
POL(SUM(x1)) = [2]x1 + x12    62.12/22.11
POL(c(x1)) = x1    62.12/22.11
POL(c1(x1)) = x1    62.12/22.11
POL(c11(x1, x2)) = x1 + x2    62.12/22.11
POL(c13(x1)) = x1    62.12/22.11
POL(c3(x1)) = x1    62.12/22.11
POL(c5(x1, x2)) = x1 + x2    62.12/22.11
POL(c9(x1)) = x1    62.12/22.11
POL(hd(x1)) = 0    62.12/22.11
POL(length(x1)) = 0    62.12/22.11
POL(nil) = 0    62.12/22.11
POL(s(x1)) = [1] + x1    62.12/22.11
POL(sum(x1)) = 0   
62.12/22.11
62.12/22.11

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 62.12/22.11
+(s(z0), z1) → s(+(z0, z1)) 62.12/22.11
++(nil, z0) → z0 62.12/22.11
++(:(z0, z1), z2) → :(z0, ++(z1, z2)) 62.12/22.11
sum(:(z0, nil)) → :(z0, nil) 62.12/22.11
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2)) 62.12/22.11
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3))))) 62.12/22.11
-(z0, 0) → z0 62.12/22.11
-(0, s(z0)) → 0 62.12/22.11
-(s(z0), s(z1)) → -(z0, z1) 62.12/22.11
quot(0, s(z0)) → 0 62.12/22.11
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1))) 62.12/22.11
length(nil) → 0 62.12/22.11
length(:(z0, z1)) → s(length(z1)) 62.12/22.11
hd(:(z0, z1)) → z0 62.12/22.11
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
S tuples:none
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0))) 62.12/22.11
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1)) 62.12/22.11
LENGTH(:(z0, z1)) → c13(LENGTH(z1)) 62.12/22.11
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) 62.12/22.11
++'(:(z0, z1), z2) → c3(++'(z1, z2)) 62.12/22.11
-'(s(z0), s(z1)) → c9(-'(z0, z1)) 62.12/22.11
+'(s(z0), z1) → c1(+'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c9, c11, c13, c

62.12/22.11
62.12/22.11

(27) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
62.12/22.11
62.12/22.11

(28) BOUNDS(O(1), O(1))

62.12/22.11
62.12/22.11
62.12/22.14 EOF