MAYBE 6.98/2.50 MAYBE 6.98/2.51 6.98/2.51 6.98/2.51 6.98/2.51 6.98/2.51 6.98/2.51 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 6.98/2.51 6.98/2.51 6.98/2.51
6.98/2.51
6.98/2.51
6.98/2.51
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
6.98/2.51 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
6.98/2.51 
↳2 CdtProblem
6.98/2.51 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
6.98/2.51 
↳4 CdtProblem
6.98/2.51 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
6.98/2.51 
↳6 CdtProblem
6.98/2.51 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
6.98/2.51 
↳8 CdtProblem
6.98/2.51
6.98/2.51 6.98/2.51
6.98/2.51
6.98/2.51

(0) Obligation:

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

lookup(Cons(x', xs'), Cons(x, xs)) → lookup(xs', xs) 6.98/2.51
lookup(Nil, Cons(x, xs)) → x 6.98/2.51
run(e, p) → intlookup(e, p) 6.98/2.51
intlookup(e, p) → intlookup(lookup(e, p), p)

Rewrite Strategy: INNERMOST
6.98/2.51
6.98/2.51

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

Converted CpxTRS to CDT
6.98/2.51
6.98/2.51

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

lookup(Cons(z0, z1), Cons(z2, z3)) → lookup(z1, z3) 6.98/2.51
lookup(Nil, Cons(z0, z1)) → z0 6.98/2.51
run(z0, z1) → intlookup(z0, z1) 6.98/2.51
intlookup(z0, z1) → intlookup(lookup(z0, z1), z1)
Tuples:

LOOKUP(Cons(z0, z1), Cons(z2, z3)) → c(LOOKUP(z1, z3)) 6.98/2.51
RUN(z0, z1) → c2(INTLOOKUP(z0, z1)) 6.98/2.51
INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1))
S tuples:

LOOKUP(Cons(z0, z1), Cons(z2, z3)) → c(LOOKUP(z1, z3)) 6.98/2.51
RUN(z0, z1) → c2(INTLOOKUP(z0, z1)) 6.98/2.51
INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1))
K tuples:none
Defined Rule Symbols:

lookup, run, intlookup

Defined Pair Symbols:

LOOKUP, RUN, INTLOOKUP

Compound Symbols:

c, c2, c3

6.98/2.51
6.98/2.51

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

RUN(z0, z1) → c2(INTLOOKUP(z0, z1))
6.98/2.52
6.98/2.52

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

lookup(Cons(z0, z1), Cons(z2, z3)) → lookup(z1, z3) 6.98/2.52
lookup(Nil, Cons(z0, z1)) → z0 6.98/2.52
run(z0, z1) → intlookup(z0, z1) 6.98/2.52
intlookup(z0, z1) → intlookup(lookup(z0, z1), z1)
Tuples:

LOOKUP(Cons(z0, z1), Cons(z2, z3)) → c(LOOKUP(z1, z3)) 6.98/2.52
INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1))
S tuples:

LOOKUP(Cons(z0, z1), Cons(z2, z3)) → c(LOOKUP(z1, z3)) 6.98/2.52
INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1))
K tuples:none
Defined Rule Symbols:

lookup, run, intlookup

Defined Pair Symbols:

LOOKUP, INTLOOKUP

Compound Symbols:

c, c3

6.98/2.52
6.98/2.52

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

Use forward instantiation to replace LOOKUP(Cons(z0, z1), Cons(z2, z3)) → c(LOOKUP(z1, z3)) by

LOOKUP(Cons(z0, Cons(y0, y1)), Cons(z2, Cons(y2, y3))) → c(LOOKUP(Cons(y0, y1), Cons(y2, y3)))
6.98/2.52
6.98/2.52

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

lookup(Cons(z0, z1), Cons(z2, z3)) → lookup(z1, z3) 6.98/2.52
lookup(Nil, Cons(z0, z1)) → z0 6.98/2.52
run(z0, z1) → intlookup(z0, z1) 6.98/2.52
intlookup(z0, z1) → intlookup(lookup(z0, z1), z1)
Tuples:

INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1)) 6.98/2.52
LOOKUP(Cons(z0, Cons(y0, y1)), Cons(z2, Cons(y2, y3))) → c(LOOKUP(Cons(y0, y1), Cons(y2, y3)))
S tuples:

INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1)) 6.98/2.52
LOOKUP(Cons(z0, Cons(y0, y1)), Cons(z2, Cons(y2, y3))) → c(LOOKUP(Cons(y0, y1), Cons(y2, y3)))
K tuples:none
Defined Rule Symbols:

lookup, run, intlookup

Defined Pair Symbols:

INTLOOKUP, LOOKUP

Compound Symbols:

c3, c

6.98/2.52
6.98/2.52

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

Use forward instantiation to replace LOOKUP(Cons(z0, Cons(y0, y1)), Cons(z2, Cons(y2, y3))) → c(LOOKUP(Cons(y0, y1), Cons(y2, y3))) by

LOOKUP(Cons(z0, Cons(z1, Cons(y1, y2))), Cons(z3, Cons(z4, Cons(y4, y5)))) → c(LOOKUP(Cons(z1, Cons(y1, y2)), Cons(z4, Cons(y4, y5))))
6.98/2.52
6.98/2.52

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

lookup(Cons(z0, z1), Cons(z2, z3)) → lookup(z1, z3) 6.98/2.52
lookup(Nil, Cons(z0, z1)) → z0 6.98/2.52
run(z0, z1) → intlookup(z0, z1) 6.98/2.52
intlookup(z0, z1) → intlookup(lookup(z0, z1), z1)
Tuples:

INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1)) 6.98/2.52
LOOKUP(Cons(z0, Cons(z1, Cons(y1, y2))), Cons(z3, Cons(z4, Cons(y4, y5)))) → c(LOOKUP(Cons(z1, Cons(y1, y2)), Cons(z4, Cons(y4, y5))))
S tuples:

INTLOOKUP(z0, z1) → c3(INTLOOKUP(lookup(z0, z1), z1), LOOKUP(z0, z1)) 6.98/2.52
LOOKUP(Cons(z0, Cons(z1, Cons(y1, y2))), Cons(z3, Cons(z4, Cons(y4, y5)))) → c(LOOKUP(Cons(z1, Cons(y1, y2)), Cons(z4, Cons(y4, y5))))
K tuples:none
Defined Rule Symbols:

lookup, run, intlookup

Defined Pair Symbols:

INTLOOKUP, LOOKUP

Compound Symbols:

c3, c

6.98/2.52
6.98/2.52
6.98/2.56 EOF