(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
lte(Cons(x', xs'), Cons(x, xs)) → lte(xs', xs)
lte(Cons(x, xs), Nil) → False
even(Cons(x, Nil)) → False
even(Cons(x', Cons(x, xs))) → even(xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lte(Nil, y) → True
even(Nil) → True
goal(x, y) → and(lte(x, y), even(x))
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
Tuples:
AND(False, False) → c
AND(True, False) → c1
AND(False, True) → c2
AND(True, True) → c3
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
LTE(Cons(z0, z1), Nil) → c5
LTE(Nil, z0) → c6
EVEN(Cons(z0, Nil)) → c7
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
EVEN(Nil) → c9
NOTEMPTY(Cons(z0, z1)) → c10
NOTEMPTY(Nil) → c11
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))
LTE(Cons(z0, z1), Nil) → c5
LTE(Nil, z0) → c6
EVEN(Cons(z0, Nil)) → c7
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
EVEN(Nil) → c9
NOTEMPTY(Cons(z0, z1)) → c10
NOTEMPTY(Nil) → c11
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:
AND, LTE, EVEN, NOTEMPTY, GOAL
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 10 trailing nodes:
LTE(Nil, z0) → c6
AND(False, False) → c
AND(True, True) → c3
AND(False, True) → c2
NOTEMPTY(Nil) → c11
EVEN(Nil) → c9
LTE(Cons(z0, z1), Nil) → c5
AND(True, False) → c1
NOTEMPTY(Cons(z0, z1)) → c10
EVEN(Cons(z0, Nil)) → c7
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
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))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
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
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
GOAL(z0, z1) → c12(LTE(z0, z1), EVEN(z0))
S tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
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
(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
GOAL(z0, z1) → c(LTE(z0, z1))
GOAL(z0, z1) → c(EVEN(z0))
S tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
GOAL(z0, z1) → c(LTE(z0, z1))
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
(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)
Removed 2 leading nodes:
GOAL(z0, z1) → c(LTE(z0, z1))
GOAL(z0, z1) → c(EVEN(z0))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
S tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
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
(11) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
S tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
LTE, EVEN
Compound Symbols:
c4, c8
(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) 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))
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))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(Cons(x1, x2)) = [5] + x2
POL(EVEN(x1)) = [5]x1
POL(LTE(x1, x2)) = [2]x2
POL(c4(x1)) = x1
POL(c8(x1)) = x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
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))
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
Defined Rule Symbols:none
Defined Pair Symbols:
LTE, EVEN
Compound Symbols:
c4, c8
(15) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(16) BOUNDS(1, 1)