YES(O(1), O(n^2)) 0.00/0.82 YES(O(1), O(n^2)) 0.00/0.85 0.00/0.85 0.00/0.85
0.00/0.85 0.00/0.850 CpxRelTRS0.00/0.85
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))0.00/0.85
↳2 CdtProblem0.00/0.85
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.85
↳4 CdtProblem0.00/0.85
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))0.00/0.85
↳6 CdtProblem0.00/0.85
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.85
↳8 CdtProblem0.00/0.85
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/0.85
↳10 CdtProblem0.00/0.85
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.85
↳12 CdtProblem0.00/0.85
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.85
↳14 BOUNDS(O(1), O(1))0.00/0.85
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))
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
Tuples:
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))
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
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))
lte, even, notEmpty, goal, and
LTE, EVEN, GOAL
c4, c8, c12
Tuples:
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))
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
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))
lte, even, notEmpty, goal, and
LTE, EVEN, GOAL
c4, c8, c12
Tuples:
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))
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
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))
lte, even, notEmpty, goal, and
LTE, EVEN, GOAL
c4, c8, c
GOAL(z0, z1) → c(LTE(z0, z1)) 0.00/0.85
GOAL(z0, z1) → c(EVEN(z0))
Tuples:
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))
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
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
lte, even, notEmpty, goal, and
LTE, EVEN
c4, c8
We considered the (Usable) Rules:none
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
The order we found is given by the following interpretation:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
POL(Cons(x1, x2)) = [1] + x2 0.00/0.85
POL(EVEN(x1)) = 0 0.00/0.85
POL(LTE(x1, x2)) = x1·x2 0.00/0.85
POL(c4(x1)) = x1 0.00/0.85
POL(c8(x1)) = x1
Tuples:
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))
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:
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
Defined Rule Symbols:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3))
lte, even, notEmpty, goal, and
LTE, EVEN
c4, c8
We considered the (Usable) Rules:none
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
The order we found is given by the following interpretation:
LTE(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
POL(Cons(x1, x2)) = [1] + x2 0.00/0.85
POL(EVEN(x1)) = [2]x1 0.00/0.85
POL(LTE(x1, x2)) = [3]x1 + [5]x2 0.00/0.85
POL(c4(x1)) = x1 0.00/0.85
POL(c8(x1)) = x1
Tuples:
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))
S tuples:none
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(Cons(z0, z1), Cons(z2, z3)) → c4(LTE(z1, z3)) 0.00/0.85
EVEN(Cons(z0, Cons(z1, z2))) → c8(EVEN(z2))
lte, even, notEmpty, goal, and
LTE, EVEN
c4, c8