WORST_CASE(Omega(n^1),O(n^1))
proof of input_MufVXBfZ49.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 164 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) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (10) CdtProblem
    (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CdtProblem
    (13) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxTRS
    (15) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
    (16) CpxTRS
    (17) CpxTrsMatchBoundsTAProof [FINISHED, 0 ms]
    (18) BOUNDS(1, n^1)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 9 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 0 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 364 ms]
    (30) BEST
        (31) proven lower bound
            (32) LowerBoundPropagationProof [FINISHED, 0 ms]
            (33) BOUNDS(n^1, INF)
        (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
            (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 66 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
            (40) BOUNDS(1, INF)


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

(0)
Obligation:
The Runtime Complexity (parallel-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(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: PARALLEL_INNERMOST
----------------------------------------

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

(2)
Obligation:
The Runtime Complexity (parallel-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(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: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(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:
   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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), 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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
K tuples:none
Defined Rule Symbols:   lte_2, even_1, notEmpty_1, goal_2, and_2

Defined Pair Symbols:   AND_2, LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6, c7, c8_1, c9, c10, c11, c12_2, c13_2


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 10 trailing nodes:
   AND(False, False) -> c
   NOTEMPTY(Nil) -> c11
   AND(True, False) -> c1
   EVEN(Cons(z0, Nil)) -> c7
   LTE(Nil, z0) -> c6
   AND(True, True) -> c3
   AND(False, True) -> c2
   NOTEMPTY(Cons(z0, z1)) -> c10
   EVEN(Nil) -> c9
   LTE(Cons(z0, z1), Nil) -> c5

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

(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(AND(lte(z0, z1), even(z0)), LTE(z0, z1))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), 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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
K tuples:none
Defined Rule Symbols:   lte_2, even_1, notEmpty_1, goal_2, and_2

Defined Pair Symbols:   LTE_2, EVEN_1, GOAL_2

Compound Symbols:   c4_1, c8_1, c12_2, c13_2


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

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

(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) -> c12(LTE(z0, z1))
   GOAL(z0, z1) -> c13(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))
   GOAL(z0, z1) -> c13(EVEN(z0))
K tuples:none
Defined Rule Symbols:   lte_2, even_1, notEmpty_1, goal_2, and_2

Defined Pair Symbols:   LTE_2, EVEN_1, GOAL_2

Compound Symbols:   c4_1, c8_1, c12_1, c13_1


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

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   GOAL(z0, z1) -> c12(LTE(z0, z1))
   GOAL(z0, z1) -> c13(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_2, even_1, notEmpty_1, goal_2, and_2

Defined Pair Symbols:   LTE_2, EVEN_1

Compound Symbols:   c4_1, c8_1


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

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
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_2, EVEN_1

Compound Symbols:   c4_1, c8_1


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

(13) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   LTE(Cons(z0, z1), Cons(z2, z3)) -> c4(LTE(z1, z3))
   EVEN(Cons(z0, Cons(z1, z2))) -> c8(EVEN(z2))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(15) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   LTE(Cons(z0, z1), Cons(z2, z3)) -> c4(LTE(z1, z3))
   EVEN(Cons(z0, Cons(z1, z2))) -> c8(EVEN(z2))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(17) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2]
transitions: 
Cons0(0, 0) -> 0
c40(0) -> 0
c80(0) -> 0
LTE0(0, 0) -> 1
EVEN0(0) -> 2
LTE1(0, 0) -> 3
c41(3) -> 1
EVEN1(0) -> 4
c81(4) -> 2
c41(3) -> 3
c81(4) -> 4

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

(18)
BOUNDS(1, n^1)

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

(19) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(20)
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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), 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))
   GOAL(z0, z1) -> c13(AND(lte(z0, z1), even(z0)), EVEN(z0))
K tuples:none
Defined Rule Symbols:   lte_2, even_1, notEmpty_1, goal_2, and_2

Defined Pair Symbols:   AND_2, LTE_2, EVEN_1, NOTEMPTY_1, GOAL_2

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6, c7, c8_1, c9, c10, c11, c12_2, c13_2


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

(21) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(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(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
----------------------------------------

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

(24)
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
----------------------------------------

(25) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(26)
Obligation:
Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9

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

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

(28)
Obligation:
Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9


Generator Equations:
gen_c4:c5:c69_14(0) <=> c5
gen_c4:c5:c69_14(+(x, 1)) <=> c4(gen_c4:c5:c69_14(x))
gen_Cons:Nil10_14(0) <=> Nil
gen_Cons:Nil10_14(+(x, 1)) <=> Cons(hole_a3_14, gen_Cons:Nil10_14(x))
gen_c7:c8:c911_14(0) <=> c7
gen_c7:c8:c911_14(+(x, 1)) <=> c8(gen_c7:c8:c911_14(x))


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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LTE(gen_Cons:Nil10_14(+(1, n13_14)), gen_Cons:Nil10_14(n13_14)) -> gen_c4:c5:c69_14(n13_14), rt in Omega(1 + n13_14)

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

Induction Step:
LTE(gen_Cons:Nil10_14(+(1, +(n13_14, 1))), gen_Cons:Nil10_14(+(n13_14, 1))) ->_R^Omega(1)
c4(LTE(gen_Cons:Nil10_14(+(1, n13_14)), gen_Cons:Nil10_14(n13_14))) ->_IH
c4(gen_c4:c5:c69_14(c14_14))

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9


Generator Equations:
gen_c4:c5:c69_14(0) <=> c5
gen_c4:c5:c69_14(+(x, 1)) <=> c4(gen_c4:c5:c69_14(x))
gen_Cons:Nil10_14(0) <=> Nil
gen_Cons:Nil10_14(+(x, 1)) <=> Cons(hole_a3_14, gen_Cons:Nil10_14(x))
gen_c7:c8:c911_14(0) <=> c7
gen_c7:c8:c911_14(+(x, 1)) <=> c8(gen_c7:c8:c911_14(x))


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

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil10_14(+(1, n13_14)), gen_Cons:Nil10_14(n13_14)) -> gen_c4:c5:c69_14(n13_14), rt in Omega(1 + n13_14)


Generator Equations:
gen_c4:c5:c69_14(0) <=> c5
gen_c4:c5:c69_14(+(x, 1)) <=> c4(gen_c4:c5:c69_14(x))
gen_Cons:Nil10_14(0) <=> Nil
gen_Cons:Nil10_14(+(x, 1)) <=> Cons(hole_a3_14, gen_Cons:Nil10_14(x))
gen_c7:c8:c911_14(0) <=> c7
gen_c7:c8:c911_14(+(x, 1)) <=> c8(gen_c7:c8:c911_14(x))


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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EVEN(gen_Cons:Nil10_14(+(1, *(2, n596_14)))) -> gen_c7:c8:c911_14(n596_14), rt in Omega(1 + n596_14)

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

Induction Step:
EVEN(gen_Cons:Nil10_14(+(1, *(2, +(n596_14, 1))))) ->_R^Omega(1)
c8(EVEN(gen_Cons:Nil10_14(+(1, *(2, n596_14))))) ->_IH
c8(gen_c7:c8:c911_14(c597_14))

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

(36)
Obligation:
Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil10_14(+(1, n13_14)), gen_Cons:Nil10_14(n13_14)) -> gen_c4:c5:c69_14(n13_14), rt in Omega(1 + n13_14)
EVEN(gen_Cons:Nil10_14(+(1, *(2, n596_14)))) -> gen_c7:c8:c911_14(n596_14), rt in Omega(1 + n596_14)


Generator Equations:
gen_c4:c5:c69_14(0) <=> c5
gen_c4:c5:c69_14(+(x, 1)) <=> c4(gen_c4:c5:c69_14(x))
gen_Cons:Nil10_14(0) <=> Nil
gen_Cons:Nil10_14(+(x, 1)) <=> Cons(hole_a3_14, gen_Cons:Nil10_14(x))
gen_c7:c8:c911_14(0) <=> c7
gen_c7:c8:c911_14(+(x, 1)) <=> c8(gen_c7:c8:c911_14(x))


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

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

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

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

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

(38)
Obligation:
Innermost TRS:
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))
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))

Types:
LTE :: Cons:Nil -> Cons:Nil -> c4:c5:c6
Cons :: a -> 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_a3_14 :: a
hole_c7:c8:c94_14 :: c7:c8:c9
hole_c10:c115_14 :: c10:c11
hole_c12:c136_14 :: c12:c13
hole_c:c1:c2:c37_14 :: c:c1:c2:c3
hole_False:True8_14 :: False:True
gen_c4:c5:c69_14 :: Nat -> c4:c5:c6
gen_Cons:Nil10_14 :: Nat -> Cons:Nil
gen_c7:c8:c911_14 :: Nat -> c7:c8:c9


Lemmas:
LTE(gen_Cons:Nil10_14(+(1, n13_14)), gen_Cons:Nil10_14(n13_14)) -> gen_c4:c5:c69_14(n13_14), rt in Omega(1 + n13_14)
EVEN(gen_Cons:Nil10_14(+(1, *(2, n596_14)))) -> gen_c7:c8:c911_14(n596_14), rt in Omega(1 + n596_14)
lte(gen_Cons:Nil10_14(+(1, n1108_14)), gen_Cons:Nil10_14(n1108_14)) -> False, rt in Omega(0)


Generator Equations:
gen_c4:c5:c69_14(0) <=> c5
gen_c4:c5:c69_14(+(x, 1)) <=> c4(gen_c4:c5:c69_14(x))
gen_Cons:Nil10_14(0) <=> Nil
gen_Cons:Nil10_14(+(x, 1)) <=> Cons(hole_a3_14, gen_Cons:Nil10_14(x))
gen_c7:c8:c911_14(0) <=> c7
gen_c7:c8:c911_14(+(x, 1)) <=> c8(gen_c7:c8:c911_14(x))


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

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

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

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

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

(40)
BOUNDS(1, INF)