MAYBE 5.48/2.03 MAYBE 5.48/2.06 5.48/2.06 5.48/2.06 5.48/2.06 5.48/2.06 5.48/2.06 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 5.48/2.06 5.48/2.06 5.48/2.06
5.48/2.06 5.48/2.06 5.48/2.06
5.48/2.06
5.48/2.06

(0) Obligation:

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

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(x, xs)) → nesteql(eql(Cons(x, xs))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(x, xs)) → eql(Cons(x, xs)) 5.48/2.06
number17(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(x) → nesteql(x)

Rewrite Strategy: INNERMOST
5.48/2.06
5.48/2.06

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

Converted CpxTRS to CDT
5.48/2.06
5.48/2.06

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
GOAL(z0) → c5(NESTEQL(z0))
S tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
GOAL(z0) → c5(NESTEQL(z0))
K tuples:none
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

NESTEQL, EQL, GOAL

Compound Symbols:

c1, c3, c5

5.48/2.06
5.48/2.06

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0) → c5(NESTEQL(z0))
5.48/2.06
5.48/2.06

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
S tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:none
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

NESTEQL, EQL

Compound Symbols:

c1, c3

5.48/2.06
5.48/2.06

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

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
We considered the (Usable) Rules:

eql(Cons(z0, z1)) → eql(Cons(z0, z1))
And the Tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
The order we found is given by the following interpretation:
Polynomial interpretation : 5.48/2.06

POL(Cons(x1, x2)) = [4]    5.48/2.06
POL(EQL(x1)) = [1]    5.48/2.06
POL(NESTEQL(x1)) = [4]x1    5.48/2.06
POL(c1(x1, x2)) = x1 + x2    5.48/2.06
POL(c3(x1)) = x1    5.48/2.06
POL(eql(x1)) = 0   
5.48/2.06
5.48/2.06

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
S tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

NESTEQL, EQL

Compound Symbols:

c1, c3

5.48/2.06
5.48/2.06

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

Use narrowing to replace NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) by

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
5.48/2.06
5.48/2.06

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
S tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

EQL, NESTEQL

Compound Symbols:

c3, c1

5.48/2.06
5.48/2.06

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

Use narrowing to replace NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) by

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
5.48/2.06
5.48/2.06

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
S tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

EQL, NESTEQL

Compound Symbols:

c3, c1

5.48/2.06
5.48/2.06

(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) by NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
5.48/2.06
5.48/2.06

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
S tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

EQL, NESTEQL

Compound Symbols:

c3, c1

5.48/2.06
5.48/2.06

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

Used rewriting to replace NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) by NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
5.48/2.06
5.48/2.06

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
Tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
S tuples:

EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:

NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Defined Rule Symbols:

nesteql, eql, number17, goal

Defined Pair Symbols:

EQL, NESTEQL

Compound Symbols:

c3, c1

5.48/2.06
5.48/2.06
5.88/2.12 EOF