WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 315 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (12) CdtProblem
    (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 31 ms]
    (16) CdtProblem
    (17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) BOUNDS(1, 1)
(19) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CpxRelTRS
    (21) SlicingProof [LOWER BOUND(ID), 0 ms]
    (22) CpxRelTRS
    (23) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) typed CpxTrs
    (25) OrderProof [LOWER BOUND(ID), 12 ms]
    (26) typed CpxTrs
    (27) RewriteLemmaProof [LOWER BOUND(ID), 365 ms]
    (28) BEST
        (29) proven lower bound
            (30) LowerBoundPropagationProof [FINISHED, 0 ms]
            (31) BOUNDS(n^1, INF)
        (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 38 ms]
            (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 13 ms]
            (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 9 ms]
            (38) BOUNDS(1, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))

Rewrite Strategy: INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
Tuples:
   AND'(False, False) -> c14
   AND'(True, False) -> c15
   AND'(False, True) -> c16
   AND'(True, True) -> c17
   AND''(False, False) -> c18
   AND''(True, False) -> c19
   AND''(False, True) -> c20
   AND''(True, True) -> c21
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   LTE'(Cons(z0, z1), Nil) -> c23
   LTE'(Nil, z0) -> c24
   EVEN'(Cons(z0, Nil)) -> c25
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   EVEN'(Nil) -> c27
   NOTEMPTY'(Cons(z0, z1)) -> c28
   NOTEMPTY'(Nil) -> c29
   GOAL'(z0, z1) -> c30(AND''(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   LTE''(Cons(z0, z1), Nil) -> c32
   LTE''(Nil, z0) -> c33
   EVEN''(Cons(z0, Nil)) -> c34
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   EVEN''(Nil) -> c36
   NOTEMPTY''(Cons(z0, z1)) -> c37
   NOTEMPTY''(Nil) -> c38
   GOAL''(z0, z1) -> c39(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   LTE''(Cons(z0, z1), Nil) -> c32
   LTE''(Nil, z0) -> c33
   EVEN''(Cons(z0, Nil)) -> c34
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   EVEN''(Nil) -> c36
   NOTEMPTY''(Cons(z0, z1)) -> c37
   NOTEMPTY''(Nil) -> c38
   GOAL''(z0, z1) -> c39(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
K tuples:none
Defined Rule Symbols:   LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2, AND_2, and_2, lte_2, even_1, notEmpty_1, goal_2

Defined Pair Symbols:   AND'_2, AND''_2, LTE'_2, EVEN'_1, NOTEMPTY'_1, GOAL'_2, LTE''_2, EVEN''_1, NOTEMPTY''_1, GOAL''_2

Compound Symbols:   c14, c15, c16, c17, c18, c19, c20, c21, c22_1, c23, c24, c25, c26_1, c27, c28, c29, c30_3, c31_1, c32, c33, c34, c35_1, c36, c37, c38, c39_4, c40_4


----------------------------------------

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 20 trailing nodes:
   EVEN''(Cons(z0, Nil)) -> c34
   EVEN'(Nil) -> c27
   AND'(True, True) -> c17
   LTE'(Cons(z0, z1), Nil) -> c23
   NOTEMPTY'(Nil) -> c29
   LTE'(Nil, z0) -> c24
   AND'(False, False) -> c14
   AND'(True, False) -> c15
   NOTEMPTY''(Cons(z0, z1)) -> c37
   AND''(True, True) -> c21
   AND''(False, True) -> c20
   NOTEMPTY'(Cons(z0, z1)) -> c28
   NOTEMPTY''(Nil) -> c38
   LTE''(Cons(z0, z1), Nil) -> c32
   AND''(False, False) -> c18
   EVEN''(Nil) -> c36
   AND''(True, False) -> c19
   LTE''(Nil, z0) -> c33
   EVEN'(Cons(z0, Nil)) -> c25
   AND'(False, True) -> c16

----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   GOAL'(z0, z1) -> c30(AND''(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL''(z0, z1) -> c39(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL''(z0, z1) -> c39(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(AND'(lte(z0, z1), even(z0)), LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
K tuples:none
Defined Rule Symbols:   LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2, AND_2, and_2, lte_2, even_1, notEmpty_1, goal_2

Defined Pair Symbols:   LTE'_2, EVEN'_1, GOAL'_2, LTE''_2, EVEN''_1, GOAL''_2

Compound Symbols:   c22_1, c26_1, c30_3, c31_1, c35_1, c39_4, c40_4


----------------------------------------

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 3 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL'(z0, z1) -> c30(LTE'(z0, z1), EVEN'(z0))
   GOAL''(z0, z1) -> c39(LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL''(z0, z1) -> c39(LTE'(z0, z1), EVEN'(z0), LTE''(z0, z1))
   GOAL''(z0, z1) -> c40(LTE'(z0, z1), EVEN'(z0), EVEN''(z0))
K tuples:none
Defined Rule Symbols:   LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2, AND_2, and_2, lte_2, even_1, notEmpty_1, goal_2

Defined Pair Symbols:   LTE'_2, EVEN'_1, LTE''_2, EVEN''_1, GOAL'_2, GOAL''_2

Compound Symbols:   c22_1, c26_1, c31_1, c35_1, c30_2, c39_3, c40_3


----------------------------------------

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL'(z0, z1) -> c14(LTE'(z0, z1))
   GOAL'(z0, z1) -> c14(EVEN'(z0))
   GOAL''(z0, z1) -> c14(LTE'(z0, z1))
   GOAL''(z0, z1) -> c14(EVEN'(z0))
   GOAL''(z0, z1) -> c14(LTE''(z0, z1))
   GOAL''(z0, z1) -> c14(EVEN''(z0))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
   GOAL''(z0, z1) -> c14(LTE'(z0, z1))
   GOAL''(z0, z1) -> c14(EVEN'(z0))
   GOAL''(z0, z1) -> c14(LTE''(z0, z1))
   GOAL''(z0, z1) -> c14(EVEN''(z0))
K tuples:none
Defined Rule Symbols:   LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2, AND_2, and_2, lte_2, even_1, notEmpty_1, goal_2

Defined Pair Symbols:   LTE'_2, EVEN'_1, LTE''_2, EVEN''_1, GOAL'_2, GOAL''_2

Compound Symbols:   c22_1, c26_1, c31_1, c35_1, c14_1


----------------------------------------

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 6 leading nodes:
   GOAL'(z0, z1) -> c14(LTE'(z0, z1))
   GOAL''(z0, z1) -> c14(LTE'(z0, z1))
   GOAL'(z0, z1) -> c14(EVEN'(z0))
   GOAL''(z0, z1) -> c14(EVEN'(z0))
   GOAL''(z0, z1) -> c14(LTE''(z0, z1))
   GOAL''(z0, z1) -> c14(EVEN''(z0))

----------------------------------------

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
K tuples:none
Defined Rule Symbols:   LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2, AND_2, and_2, lte_2, even_1, notEmpty_1, goal_2

Defined Pair Symbols:   LTE'_2, EVEN'_1, LTE''_2, EVEN''_1

Compound Symbols:   c22_1, c26_1, c31_1, c35_1


----------------------------------------

(13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))

----------------------------------------

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
S tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   LTE'_2, EVEN'_1, LTE''_2, EVEN''_1

Compound Symbols:   c22_1, c26_1, c31_1, c35_1


----------------------------------------

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
We considered the (Usable) Rules:none
And the Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(Cons(x_1, x_2)) = [1] + x_2
   POL(EVEN'(x_1)) = x_1
   POL(EVEN''(x_1)) = x_1
   POL(LTE'(x_1, x_2)) = x_1 + x_2
   POL(LTE''(x_1, x_2)) = x_1
   POL(c22(x_1)) = x_1
   POL(c26(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c35(x_1)) = x_1

----------------------------------------

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   LTE'(Cons(z0, z1), Cons(z2, z3)) -> c22(LTE'(z1, z3))
   EVEN'(Cons(z0, Cons(z1, z2))) -> c26(EVEN'(z2))
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
S tuples:none
K tuples:
   LTE''(Cons(z0, z1), Cons(z2, z3)) -> c31(LTE''(z1, z3))
   EVEN''(Cons(z0, Cons(z1, z2))) -> c35(EVEN''(z2))
Defined Rule Symbols:none

Defined Pair Symbols:   LTE'_2, EVEN'_1, LTE''_2, EVEN''_1

Compound Symbols:   c22_1, c26_1, c31_1, c35_1


----------------------------------------

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(18)
BOUNDS(1, 1)

----------------------------------------

(19) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(20)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   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))

Rewrite Strategy: INNERMOST
----------------------------------------

(21) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
Cons/0

----------------------------------------

(22)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
   LTE(Cons(z1), Nil) -> c5
   LTE(Nil, z0) -> c6
   EVEN(Cons(Nil)) -> c7
   EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
   EVEN(Nil) -> c9
   NOTEMPTY(Cons(z1)) -> c10
   NOTEMPTY(Nil) -> c11
   GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
   lte(Cons(z1), Nil) -> False
   lte(Nil, z0) -> True
   even(Cons(Nil)) -> False
   even(Cons(Cons(z2))) -> even(z2)
   even(Nil) -> True
   notEmpty(Cons(z1)) -> True
   notEmpty(Nil) -> False
   goal(z0, z1) -> and(lte(z0, z1), even(z0))

Rewrite Strategy: INNERMOST
----------------------------------------

(23) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9

----------------------------------------

(25) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LTE, EVEN, lte, even
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9


Generator Equations:
gen_c4:c5:c68_14(0) <=> c5
gen_c4:c5:c68_14(+(x, 1)) <=> c4(gen_c4:c5:c68_14(x))
gen_Cons:Nil9_14(0) <=> Nil
gen_Cons:Nil9_14(+(x, 1)) <=> Cons(gen_Cons:Nil9_14(x))
gen_c7:c8:c910_14(0) <=> c7
gen_c7:c8:c910_14(+(x, 1)) <=> c8(gen_c7:c8:c910_14(x))


The following defined symbols remain to be analysed:
LTE, EVEN, lte, even
----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LTE(gen_Cons:Nil9_14(+(1, n12_14)), gen_Cons:Nil9_14(n12_14)) -> gen_c4:c5:c68_14(n12_14), rt in Omega(1 + n12_14)

Induction Base:
LTE(gen_Cons:Nil9_14(+(1, 0)), gen_Cons:Nil9_14(0)) ->_R^Omega(1)
c5

Induction Step:
LTE(gen_Cons:Nil9_14(+(1, +(n12_14, 1))), gen_Cons:Nil9_14(+(n12_14, 1))) ->_R^Omega(1)
c4(LTE(gen_Cons:Nil9_14(+(1, n12_14)), gen_Cons:Nil9_14(n12_14))) ->_IH
c4(gen_c4:c5:c68_14(c13_14))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(28)
Complex Obligation (BEST)

----------------------------------------

(29)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9


Generator Equations:
gen_c4:c5:c68_14(0) <=> c5
gen_c4:c5:c68_14(+(x, 1)) <=> c4(gen_c4:c5:c68_14(x))
gen_Cons:Nil9_14(0) <=> Nil
gen_Cons:Nil9_14(+(x, 1)) <=> Cons(gen_Cons:Nil9_14(x))
gen_c7:c8:c910_14(0) <=> c7
gen_c7:c8:c910_14(+(x, 1)) <=> c8(gen_c7:c8:c910_14(x))


The following defined symbols remain to be analysed:
LTE, EVEN, lte, even
----------------------------------------

(30) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(31)
BOUNDS(n^1, INF)

----------------------------------------

(32)
Obligation:
Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil9_14(+(1, n12_14)), gen_Cons:Nil9_14(n12_14)) -> gen_c4:c5:c68_14(n12_14), rt in Omega(1 + n12_14)


Generator Equations:
gen_c4:c5:c68_14(0) <=> c5
gen_c4:c5:c68_14(+(x, 1)) <=> c4(gen_c4:c5:c68_14(x))
gen_Cons:Nil9_14(0) <=> Nil
gen_Cons:Nil9_14(+(x, 1)) <=> Cons(gen_Cons:Nil9_14(x))
gen_c7:c8:c910_14(0) <=> c7
gen_c7:c8:c910_14(+(x, 1)) <=> c8(gen_c7:c8:c910_14(x))


The following defined symbols remain to be analysed:
EVEN, lte, even
----------------------------------------

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EVEN(gen_Cons:Nil9_14(+(1, *(2, n559_14)))) -> gen_c7:c8:c910_14(n559_14), rt in Omega(1 + n559_14)

Induction Base:
EVEN(gen_Cons:Nil9_14(+(1, *(2, 0)))) ->_R^Omega(1)
c7

Induction Step:
EVEN(gen_Cons:Nil9_14(+(1, *(2, +(n559_14, 1))))) ->_R^Omega(1)
c8(EVEN(gen_Cons:Nil9_14(+(1, *(2, n559_14))))) ->_IH
c8(gen_c7:c8:c910_14(c560_14))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(34)
Obligation:
Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil9_14(+(1, n12_14)), gen_Cons:Nil9_14(n12_14)) -> gen_c4:c5:c68_14(n12_14), rt in Omega(1 + n12_14)
EVEN(gen_Cons:Nil9_14(+(1, *(2, n559_14)))) -> gen_c7:c8:c910_14(n559_14), rt in Omega(1 + n559_14)


Generator Equations:
gen_c4:c5:c68_14(0) <=> c5
gen_c4:c5:c68_14(+(x, 1)) <=> c4(gen_c4:c5:c68_14(x))
gen_Cons:Nil9_14(0) <=> Nil
gen_Cons:Nil9_14(+(x, 1)) <=> Cons(gen_Cons:Nil9_14(x))
gen_c7:c8:c910_14(0) <=> c7
gen_c7:c8:c910_14(+(x, 1)) <=> c8(gen_c7:c8:c910_14(x))


The following defined symbols remain to be analysed:
lte, even
----------------------------------------

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lte(gen_Cons:Nil9_14(+(1, n1026_14)), gen_Cons:Nil9_14(n1026_14)) -> False, rt in Omega(0)

Induction Base:
lte(gen_Cons:Nil9_14(+(1, 0)), gen_Cons:Nil9_14(0)) ->_R^Omega(0)
False

Induction Step:
lte(gen_Cons:Nil9_14(+(1, +(n1026_14, 1))), gen_Cons:Nil9_14(+(n1026_14, 1))) ->_R^Omega(0)
lte(gen_Cons:Nil9_14(+(1, n1026_14)), gen_Cons:Nil9_14(n1026_14)) ->_IH
False

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(36)
Obligation:
Innermost TRS:
Rules:
LTE(Cons(z1), Cons(z3)) -> c4(LTE(z1, z3))
LTE(Cons(z1), Nil) -> c5
LTE(Nil, z0) -> c6
EVEN(Cons(Nil)) -> c7
EVEN(Cons(Cons(z2))) -> c8(EVEN(z2))
EVEN(Nil) -> c9
NOTEMPTY(Cons(z1)) -> c10
NOTEMPTY(Nil) -> c11
GOAL(z0, z1) -> c12(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
lte(Cons(z1), Cons(z3)) -> lte(z1, z3)
lte(Cons(z1), Nil) -> False
lte(Nil, z0) -> True
even(Cons(Nil)) -> False
even(Cons(Cons(z2))) -> even(z2)
even(Nil) -> True
notEmpty(Cons(z1)) -> True
notEmpty(Nil) -> False
goal(z0, z1) -> and(lte(z0, z1), even(z0))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: Cons:Nil -> Cons:Nil
c4 :: c4:c5:c6 -> c4:c5:c6
Nil :: Cons:Nil
c5 :: c4:c5:c6
c6 :: c4:c5:c6
EVEN :: Cons:Nil -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9 -> c7:c8:c9
c9 :: c7:c8:c9
NOTEMPTY :: Cons:Nil -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
GOAL :: Cons:Nil -> Cons:Nil -> c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6 -> c12:c13
AND :: False:True -> False:True -> c:c1:c2:c3
lte :: Cons:Nil -> Cons:Nil -> False:True
even :: Cons:Nil -> False:True
c13 :: c:c1:c2:c3 -> c7:c8:c9 -> c12:c13
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
notEmpty :: Cons:Nil -> False:True
goal :: Cons:Nil -> Cons:Nil -> False:True
hole_c4:c5:c61_14 :: c4:c5:c6
hole_Cons:Nil2_14 :: Cons:Nil
hole_c7:c8:c93_14 :: c7:c8:c9
hole_c10:c114_14 :: c10:c11
hole_c12:c135_14 :: c12:c13
hole_c:c1:c2:c36_14 :: c:c1:c2:c3
hole_False:True7_14 :: False:True
gen_c4:c5:c68_14 :: Nat -> c4:c5:c6
gen_Cons:Nil9_14 :: Nat -> Cons:Nil
gen_c7:c8:c910_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil9_14(+(1, n12_14)), gen_Cons:Nil9_14(n12_14)) -> gen_c4:c5:c68_14(n12_14), rt in Omega(1 + n12_14)
EVEN(gen_Cons:Nil9_14(+(1, *(2, n559_14)))) -> gen_c7:c8:c910_14(n559_14), rt in Omega(1 + n559_14)
lte(gen_Cons:Nil9_14(+(1, n1026_14)), gen_Cons:Nil9_14(n1026_14)) -> False, rt in Omega(0)


Generator Equations:
gen_c4:c5:c68_14(0) <=> c5
gen_c4:c5:c68_14(+(x, 1)) <=> c4(gen_c4:c5:c68_14(x))
gen_Cons:Nil9_14(0) <=> Nil
gen_Cons:Nil9_14(+(x, 1)) <=> Cons(gen_Cons:Nil9_14(x))
gen_c7:c8:c910_14(0) <=> c7
gen_c7:c8:c910_14(+(x, 1)) <=> c8(gen_c7:c8:c910_14(x))


The following defined symbols remain to be analysed:
even
----------------------------------------

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
even(gen_Cons:Nil9_14(+(1, *(2, n1357_14)))) -> False, rt in Omega(0)

Induction Base:
even(gen_Cons:Nil9_14(+(1, *(2, 0)))) ->_R^Omega(0)
False

Induction Step:
even(gen_Cons:Nil9_14(+(1, *(2, +(n1357_14, 1))))) ->_R^Omega(0)
even(gen_Cons:Nil9_14(+(1, *(2, n1357_14)))) ->_IH
False

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(38)
BOUNDS(1, INF)