Runtime Complexity (innermost) proof of /tmp/tmpcN0SEL/10.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

0 CpxTRS

↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 13 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtUsableRulesProof (⇔, 0 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 214 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 55 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 55 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 196 ms)

↳24 CdtProblem

↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 219 ms)

↳26 CdtProblem

↳27 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳28 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

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

Rewrite Strategy: INNERMOST

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

The following defined symbols can occur below the 0th argument of +: +
The following defined symbols can occur below the 1th argument of +: +
The following defined symbols can occur below the 0th argument of sum: +
The following defined symbols can occur below the 0th argument of quot: hd, sum, +, -, length
The following defined symbols can occur below the 1th argument of quot: length
The following defined symbols can occur below the 0th argument of hd: sum, +
The following defined symbols can occur below the 0th argument of -: hd, sum, +, -
The following defined symbols can occur below the 1th argument of -: length

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

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

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
++'(nil, z0) → c1
-'(s(z0), s(z1)) → c2(-'(z0, z1))
-'(0, s(z0)) → c3
-'(z0, 0) → c4
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
LENGTH(nil) → c6
QUOT(0, s(z0)) → c7
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
+'(s(z0), z1) → c10(+'(z0, z1))
+'(0, z0) → c11
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(:(z0, nil)) → c13
HD(:(z0, z1)) → c14

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
++'(nil, z0) → c1
-'(s(z0), s(z1)) → c2(-'(z0, z1))
-'(0, s(z0)) → c3
-'(z0, 0) → c4
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
LENGTH(nil) → c6
QUOT(0, s(z0)) → c7
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
+'(s(z0), z1) → c10(+'(z0, z1))
+'(0, z0) → c11
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(:(z0, nil)) → c13
HD(:(z0, z1)) → c14

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

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

Removed 8 trailing nodes:

-'(0, s(z0)) → c3
SUM(:(z0, nil)) → c13
QUOT(0, s(z0)) → c7
-'(z0, 0) → c4
LENGTH(nil) → c6
+'(0, z0) → c11
++'(nil, z0) → c1
HD(:(z0, z1)) → c14

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c9, c10, c12

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

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), SUM(z0), LENGTH(z0))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c9(QUOT(hd(sum(z0)), length(z0)), SUM(z0), LENGTH(z0))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c9

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c1(SUM(z0))
AVG(z0) → c1(LENGTH(z0))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c1(SUM(z0))
AVG(z0) → c1(LENGTH(z0))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

AVG(z0) → c1(LENGTH(z0))
AVG(z0) → c1(SUM(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

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

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

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
length(:(z0, z1)) → s(length(z1))
length(nil) → 0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
hd(:(z0, z1)) → z0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

++(:(z0, z1), z2) → :(z0, ++(z1, z2))
++(nil, z0) → z0
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
avg(z0) → quot(hd(sum(z0)), length(z0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

++'(:(z0, z1), z2) → c(++'(z1, z2))

We considered the (Usable) Rules:none
And the Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x₁, x₂)) = 0
POL(+'(x₁, x₂)) = 0
POL(++'(x₁, x₂)) = x₁
POL(-(x₁, x₂)) = 0
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(:(x₁, x₂)) = [1] + x₂
POL(AVG(x₁)) = 0
POL(LENGTH(x₁)) = 0
POL(QUOT(x₁, x₂)) = 0
POL(SUM(x₁)) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = 0
POL(length(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(sum(x₁)) = 0

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
++'(:(z0, z1), z2) → c(++'(z1, z2))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

LENGTH(:(z0, z1)) → c5(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x₁, x₂)) = 0
POL(+'(x₁, x₂)) = 0
POL(++'(x₁, x₂)) = 0
POL(-(x₁, x₂)) = [1] + x₁
POL(-'(x₁, x₂)) = 0
POL(0) = [1]
POL(:(x₁, x₂)) = [1] + x₂
POL(AVG(x₁)) = x₁
POL(LENGTH(x₁)) = x₁
POL(QUOT(x₁, x₂)) = 0
POL(SUM(x₁)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = 0
POL(length(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = x₁
POL(sum(x₁)) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

-'(s(z0), s(z1)) → c2(-'(z0, z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
++'(:(z0, z1), z2) → c(++'(z1, z2))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(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)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))

We considered the (Usable) Rules:

-(0, s(z0)) → 0
+(s(z0), z1) → s(+(z0, z1))
-(s(z0), s(z1)) → -(z0, z1)
-(z0, 0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
+(0, z0) → z0
hd(:(z0, z1)) → z0

And the Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = 0
POL(++'(x₁, x₂)) = x₁
POL(-(x₁, x₂)) = x₁
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(:(x₁, x₂)) = [1] + x₁ + x₂
POL(AVG(x₁)) = [3] + [3]x₁
POL(LENGTH(x₁)) = 0
POL(QUOT(x₁, x₂)) = [1] + [2]x₁
POL(SUM(x₁)) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = x₁
POL(length(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = [1] + x₁
POL(sum(x₁)) = [1] + x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

-'(s(z0), s(z1)) → c2(-'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
++'(:(z0, z1), z2) → c(++'(z1, z2))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

+'(s(z0), z1) → c10(+'(z0, z1))

We considered the (Usable) Rules:

+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0

And the Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = [1] + [2]x₁ + x₂
POL(++'(x₁, x₂)) = x₁·x₂ + x₁²
POL(-(x₁, x₂)) = [2]x₂ + [2]x₂²
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(:(x₁, x₂)) = [1] + x₁ + x₂
POL(AVG(x₁)) = [2]
POL(LENGTH(x₁)) = 0
POL(QUOT(x₁, x₂)) = [1]
POL(SUM(x₁)) = [2]x₁²
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = 0
POL(length(x₁)) = [2] + [2]x₁²
POL(nil) = [1]
POL(s(x₁)) = [2] + x₁
POL(sum(x₁)) = [2]

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:

-'(s(z0), s(z1)) → c2(-'(z0, z1))

K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
++'(:(z0, z1), z2) → c(++'(z1, z2))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

(25) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

-'(s(z0), s(z1)) → c2(-'(z0, z1))

We considered the (Usable) Rules:

-(0, s(z0)) → 0
+(s(z0), z1) → s(+(z0, z1))
-(s(z0), s(z1)) → -(z0, z1)
-(z0, 0) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
length(:(z0, z1)) → s(length(z1))
sum(:(z0, nil)) → :(z0, nil)
length(nil) → 0
+(0, z0) → z0
hd(:(z0, z1)) → z0

And the Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = 0
POL(++'(x₁, x₂)) = x₁·x₂
POL(-(x₁, x₂)) = x₁
POL(-'(x₁, x₂)) = [1] + [2]x₂
POL(0) = 0
POL(:(x₁, x₂)) = [1] + x₁ + x₂
POL(AVG(x₁)) = [2]x₁²
POL(LENGTH(x₁)) = x₁²
POL(QUOT(x₁, x₂)) = [2]x₁·x₂
POL(SUM(x₁)) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = x₁
POL(length(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = [1] + x₁
POL(sum(x₁)) = x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(s(z0), s(z1)) → -(z0, z1)
-(0, s(z0)) → 0
-(z0, 0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(0, z0) → z0
hd(:(z0, z1)) → z0
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(:(z0, nil)) → :(z0, nil)
length(:(z0, z1)) → s(length(z1))
length(nil) → 0

Tuples:

++'(:(z0, z1), z2) → c(++'(z1, z2))
-'(s(z0), s(z1)) → c2(-'(z0, z1))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))

S tuples:none
K tuples:

AVG(z0) → c1(QUOT(hd(sum(z0)), length(z0)))
++'(:(z0, z1), z2) → c(++'(z1, z2))
LENGTH(:(z0, z1)) → c5(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c12(SUM(:(+(z0, z1), z2)), +'(z0, z1))
QUOT(s(z0), s(z1)) → c8(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
+'(s(z0), z1) → c10(+'(z0, z1))
-'(s(z0), s(z1)) → c2(-'(z0, z1))

Defined Rule Symbols:

-, +, hd, sum, length

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c5, c8, c10, c12, c1

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

The set S is empty

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(12) Obligation:

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

(14) Obligation:

(15) CdtUsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(18) Obligation:

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(20) Obligation:

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(22) Obligation:

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(24) Obligation:

(25) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(26) Obligation:

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

(28) BOUNDS(1, 1)