YES(O(1), O(n^3)) 4.88/1.86 YES(O(1), O(n^3)) 4.88/1.88 4.88/1.88 4.88/1.88 4.88/1.88 4.88/1.89 4.88/1.89 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 4.88/1.89 4.88/1.89 4.88/1.89
4.88/1.89 4.88/1.89 4.88/1.89
4.88/1.89
4.88/1.89

(0) Obligation:

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

mul0(C(x, y), y') → add0(mul0(y, y'), y') 4.88/1.89
mul0(Z, y) → Z 4.88/1.89
add0(C(x, y), y') → add0(y, C(S, y')) 4.88/1.89
add0(Z, y) → y 4.88/1.89
second(C(x, y)) → y 4.88/1.89
isZero(C(x, y)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(xs, ys) → mul0(xs, ys)

Rewrite Strategy: INNERMOST
4.88/1.89
4.88/1.89

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

Converted CpxTRS to CDT
4.88/1.89
4.88/1.89

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2))) 4.88/1.89
GOAL(z0, z1) → c7(MUL0(z0, z1))
S tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2))) 4.88/1.89
GOAL(z0, z1) → c7(MUL0(z0, z1))
K tuples:none
Defined Rule Symbols:

mul0, add0, second, isZero, goal

Defined Pair Symbols:

MUL0, ADD0, GOAL

Compound Symbols:

c, c2, c7

4.88/1.89
4.88/1.89

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c7(MUL0(z0, z1))
4.88/1.89
4.88/1.89

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
S tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
K tuples:none
Defined Rule Symbols:

mul0, add0, second, isZero, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.88/1.89
4.88/1.89

(5) 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.

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))
We considered the (Usable) Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0
And the Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.88/1.89

POL(ADD0(x1, x2)) = [1]    4.88/1.89
POL(C(x1, x2)) = [2] + x1 + x2    4.88/1.89
POL(MUL0(x1, x2)) = [2]x1    4.88/1.89
POL(S) = [3]    4.88/1.89
POL(Z) = [3]    4.88/1.89
POL(add0(x1, x2)) = [3]    4.88/1.89
POL(c(x1, x2)) = x1 + x2    4.88/1.89
POL(c2(x1)) = x1    4.88/1.89
POL(mul0(x1, x2)) = 0   
4.88/1.89
4.88/1.89

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
S tuples:

ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
K tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))
Defined Rule Symbols:

mul0, add0, second, isZero, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.88/1.89
4.88/1.89

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
We considered the (Usable) Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0
And the Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.88/1.89

POL(ADD0(x1, x2)) = x1    4.88/1.89
POL(C(x1, x2)) = [1] + x2    4.88/1.89
POL(MUL0(x1, x2)) = x12·x2 + x1·x22    4.88/1.89
POL(S) = 0    4.88/1.89
POL(Z) = 0    4.88/1.89
POL(add0(x1, x2)) = x1 + x2    4.88/1.89
POL(c(x1, x2)) = x1 + x2    4.88/1.89
POL(c2(x1)) = x1    4.88/1.89
POL(mul0(x1, x2)) = x2 + x1·x2   
4.88/1.89
4.88/1.89

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
Tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
S tuples:none
K tuples:

MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
Defined Rule Symbols:

mul0, add0, second, isZero, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.88/1.89
4.88/1.89

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

The set S is empty
4.88/1.89
4.88/1.89

(10) BOUNDS(O(1), O(1))

4.88/1.89
4.88/1.89
5.17/1.96 EOF