4.87/1.88 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

4.87/1.88

4.87/1.88
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

0 CpxTRS

4.87/1.88

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

4.87/1.88

↳2 CdtProblem

4.87/1.88

↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)

4.87/1.88

↳4 CdtProblem

4.87/1.89

↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

4.87/1.89

↳6 CdtProblem

4.87/1.89

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

4.87/1.89

↳8 CdtProblem

4.87/1.89

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

4.87/1.89

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

4.87/1.89

4.87/1.89 4.87/1.89

4.87/1.89

(0) Obligation:

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

mul0(Cons(x, xs), y) → add0(mul0(xs, y), y) 4.87/1.89
add0(Cons(x, xs), y) → add0(xs, Cons(S, y)) 4.87/1.89
mul0(Nil, y) → Nil 4.87/1.89
add0(Nil, y) → y 4.87/1.89
goal(xs, ys) → mul0(xs, ys)

Rewrite Strategy: INNERMOST

4.87/1.89

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

Converted CpxTRS to CDT

4.87/1.89

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0 4.87/1.89
goal(z0, z1) → mul0(z0, z1)

Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2))) 4.87/1.89
GOAL(z0, z1) → c4(MUL0(z0, z1))

S tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2))) 4.87/1.89
GOAL(z0, z1) → c4(MUL0(z0, z1))

K tuples:none
Defined Rule Symbols:

mul0, add0, goal

Defined Pair Symbols:

MUL0, ADD0, GOAL

Compound Symbols:

c, c2, c4

4.87/1.89

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c4(MUL0(z0, z1))

4.87/1.89

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0 4.87/1.89
goal(z0, z1) → mul0(z0, z1)

Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

S tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

K tuples:none
Defined Rule Symbols:

mul0, add0, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.87/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(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))

We considered the (Usable) Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0

And the Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

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

POL(ADD0(x₁, x₂)) = [1] 4.87/1.89
POL(Cons(x₁, x₂)) = [2] + x₁ + x₂ 4.87/1.89
POL(MUL0(x₁, x₂)) = [2]x₁ 4.87/1.89
POL(Nil) = [3] 4.87/1.89
POL(S) = [3] 4.87/1.89
POL(add0(x₁, x₂)) = [3] 4.87/1.89
POL(c(x₁, x₂)) = x₁ + x₂ 4.87/1.89
POL(c2(x₁)) = x₁ 4.87/1.89
POL(mul0(x₁, x₂)) = 0

4.87/1.89

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0 4.87/1.89
goal(z0, z1) → mul0(z0, z1)

Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

S tuples:

ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

K tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))

Defined Rule Symbols:

mul0, add0, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.87/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(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

We considered the (Usable) Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0

And the Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

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

POL(ADD0(x₁, x₂)) = x₁ 4.87/1.89
POL(Cons(x₁, x₂)) = [1] + x₂ 4.87/1.89
POL(MUL0(x₁, x₂)) = x₁²·x₂ + x₁·x₂² 4.87/1.89
POL(Nil) = 0 4.87/1.89
POL(S) = 0 4.87/1.89
POL(add0(x₁, x₂)) = x₁ + x₂ 4.87/1.89
POL(c(x₁, x₂)) = x₁ + x₂ 4.87/1.89
POL(c2(x₁)) = x₁ 4.87/1.89
POL(mul0(x₁, x₂)) = x₂ + x₁·x₂

4.87/1.89

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

mul0(Cons(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.87/1.89
mul0(Nil, z0) → Nil 4.87/1.89
add0(Cons(z0, z1), z2) → add0(z1, Cons(S, z2)) 4.87/1.89
add0(Nil, z0) → z0 4.87/1.89
goal(z0, z1) → mul0(z0, z1)

Tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

S tuples:none
K tuples:

MUL0(Cons(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.87/1.89
ADD0(Cons(z0, z1), z2) → c2(ADD0(z1, Cons(S, z2)))

Defined Rule Symbols:

mul0, add0, goal

Defined Pair Symbols:

MUL0, ADD0

Compound Symbols:

c, c2

4.87/1.89

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

The set S is empty

4.87/1.89

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

4.87/1.89