0.00/0.85 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

0.00/0.85

0.00/0.85
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS

0.00/0.85

↳1 CpxRelTrsToCDT (UPPER BOUND (ID))

0.00/0.85

↳2 CdtProblem

0.00/0.85

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

0.00/0.85

↳4 CdtProblem

0.00/0.85

↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))

0.00/0.85

↳6 CdtProblem

0.00/0.85

↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)

0.00/0.85

↳8 CdtProblem

0.00/0.85

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

0.00/0.85

↳10 CdtProblem

0.00/0.85

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

0.00/0.85

↳12 CdtProblem

0.00/0.85

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

0.00/0.85

↳14 BOUNDS(O(1), O(1))

0.00/0.85

0.00/0.85 0.00/0.85

0.00/0.85

(0) Obligation:

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

lte(Cons(x', xs'), Cons(x, xs)) → lte(xs', xs) 0.00/0.85
lte(Cons(x, xs), Nil) → False 0.00/0.85
even(Cons(x, Nil)) → False 0.00/0.85
even(Cons(x', Cons(x, xs))) → even(xs) 0.00/0.85
notEmpty(Cons(x, xs)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
lte(Nil, y) → True 0.00/0.85
even(Nil) → True 0.00/0.85
goal(x, y) → and(lte(x, y), even(x))

The (relative) TRS S consists of the following rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True

Rewrite Strategy: INNERMOST

0.00/0.85

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.

0.00/0.85

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))

S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))

K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c4, c8, c12

0.00/0.85

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

Removed 1 trailing tuple parts

0.00/0.85

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c12(LTE(z0, z1), EVEN(z0))

S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c12(LTE(z0, z1), EVEN(z0))

K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c4, c8, c12

0.00/0.85

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

Split RHS of tuples not part of any SCC

0.00/0.85

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c(LTE(z0, z1)) 0.00/0.85
GOAL(z0, z1) → c(EVEN(z0))

S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2)) 0.00/0.85
GOAL(z0, z1) → c(LTE(z0, z1)) 0.00/0.85
GOAL(z0, z1) → c(EVEN(z0))

K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c4, c8, c

0.00/0.85

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c(LTE(z0, z1)) 0.00/0.85
GOAL(z0, z1) → c(EVEN(z0))

0.00/0.85

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c4, c8

0.00/0.85

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))

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

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

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

POL(Cons(x₁, x₂)) = [1] + x₂ 0.00/0.85
POL(EVEN(x₁)) = 0 0.00/0.85
POL(LTE(x₁, x₂)) = x₁·x₂ 0.00/0.85
POL(c4(x₁)) = x₁ 0.00/0.85
POL(c8(x₁)) = x₁

0.00/0.85

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

S tuples:

EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

K tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))

Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c4, c8

0.00/0.85

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

EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

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

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

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

POL(Cons(x₁, x₂)) = [1] + x₂ 0.00/0.85
POL(EVEN(x₁)) = [2]x₁ 0.00/0.85
POL(LTE(x₁, x₂)) = [3]x₁ + [5]x₂ 0.00/0.85
POL(c4(x₁)) = x₁ 0.00/0.85
POL(c8(x₁)) = x₁

0.00/0.85

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 0.00/0.85
and(True, False) → False 0.00/0.85
and(False, True) → False 0.00/0.85
and(True, True) → True 0.00/0.85
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3) 0.00/0.85
lte(Cons(z0, z1), Nil) → False 0.00/0.85
lte(Nil, z0) → True 0.00/0.85
even(Cons(z0, Nil)) → False 0.00/0.85
even(Cons(z0, Cons(z1, z2))) → even(z2) 0.00/0.85
even(Nil) → True 0.00/0.85
notEmpty(Cons(z0, z1)) → True 0.00/0.85
notEmpty(Nil) → False 0.00/0.85
goal(z0, z1) → and(lte(z0, z1), even(z0))

Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

S tuples:none
K tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))

Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c4, c8

0.00/0.85

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

The set S is empty

0.00/0.85

(14) BOUNDS(O(1), O(1))

0.00/0.85