WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox2/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), 395 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) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 17 ms]
    (14) CdtProblem
    (15) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) BOUNDS(1, 1)
(17) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) CpxRelTRS
    (19) SlicingProof [LOWER BOUND(ID), 0 ms]
    (20) CpxRelTRS
    (21) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) typed CpxTrs
    (23) OrderProof [LOWER BOUND(ID), 26 ms]
    (24) typed CpxTrs
    (25) RewriteLemmaProof [LOWER BOUND(ID), 333 ms]
    (26) BEST
        (27) proven lower bound
            (28) LowerBoundPropagationProof [FINISHED, 0 ms]
            (29) BOUNDS(n^1, INF)
        (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 84 ms]
            (32) typed CpxTrs


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

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

   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22

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

   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil

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:

   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22

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

   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil
   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22
Tuples:
   A__EQ'(0, 0) -> c23
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   A__EQ'(z0, z1) -> c25
   A__EQ'(z0, z1) -> c26
   A__INF'(z0) -> c27
   A__INF'(z0) -> c28
   A__TAKE'(0, z0) -> c29
   A__TAKE'(s(z0), cons(z1, z2)) -> c30
   A__TAKE'(z0, z1) -> c31
   A__LENGTH'(nil) -> c32
   A__LENGTH'(cons(z0, z1)) -> c33
   A__LENGTH'(z0) -> c34
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   MARK'(inf(z0)) -> c36(A__INF'(mark(z0)), MARK'(z0))
   MARK'(take(z0, z1)) -> c37(A__TAKE'(mark(z0), mark(z1)), MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(A__LENGTH'(mark(z0)), MARK'(z0))
   MARK'(0) -> c39
   MARK'(true) -> c40
   MARK'(s(z0)) -> c41
   MARK'(false) -> c42
   MARK'(cons(z0, z1)) -> c43
   MARK'(nil) -> c44
   A__EQ''(0, 0) -> c45
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   A__EQ''(z0, z1) -> c47
   A__EQ''(z0, z1) -> c48
   A__INF''(z0) -> c49
   A__INF''(z0) -> c50
   A__TAKE''(0, z0) -> c51
   A__TAKE''(s(z0), cons(z1, z2)) -> c52
   A__TAKE''(z0, z1) -> c53
   A__LENGTH''(nil) -> c54
   A__LENGTH''(cons(z0, z1)) -> c55
   A__LENGTH''(z0) -> c56
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(A__INF''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(A__LENGTH''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(0) -> c62
   MARK''(true) -> c63
   MARK''(s(z0)) -> c64
   MARK''(false) -> c65
   MARK''(cons(z0, z1)) -> c66
   MARK''(nil) -> c67
S tuples:
   A__EQ''(0, 0) -> c45
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   A__EQ''(z0, z1) -> c47
   A__EQ''(z0, z1) -> c48
   A__INF''(z0) -> c49
   A__INF''(z0) -> c50
   A__TAKE''(0, z0) -> c51
   A__TAKE''(s(z0), cons(z1, z2)) -> c52
   A__TAKE''(z0, z1) -> c53
   A__LENGTH''(nil) -> c54
   A__LENGTH''(cons(z0, z1)) -> c55
   A__LENGTH''(z0) -> c56
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(A__INF''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(A__LENGTH''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(0) -> c62
   MARK''(true) -> c63
   MARK''(s(z0)) -> c64
   MARK''(false) -> c65
   MARK''(cons(z0, z1)) -> c66
   MARK''(nil) -> c67
K tuples:none
Defined Rule Symbols:   A__EQ_2, A__INF_1, A__TAKE_2, A__LENGTH_1, MARK_1, a__eq_2, a__inf_1, a__take_2, a__length_1, mark_1

Defined Pair Symbols:   A__EQ'_2, A__INF'_1, A__TAKE'_2, A__LENGTH'_1, MARK'_1, A__EQ''_2, A__INF''_1, A__TAKE''_2, A__LENGTH''_1, MARK''_1

Compound Symbols:   c23, c24_1, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35_1, c36_2, c37_3, c38_2, c39, c40, c41, c42, c43, c44, c45, c46_1, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57_1, c58_3, c59_4, c60_4, c61_3, c62, c63, c64, c65, c66, c67


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 34 trailing nodes:
   MARK''(s(z0)) -> c64
   A__INF''(z0) -> c50
   A__EQ'(0, 0) -> c23
   MARK'(false) -> c42
   MARK'(cons(z0, z1)) -> c43
   A__TAKE''(s(z0), cons(z1, z2)) -> c52
   A__TAKE'(z0, z1) -> c31
   A__INF'(z0) -> c28
   MARK''(nil) -> c67
   A__LENGTH'(cons(z0, z1)) -> c33
   MARK''(true) -> c63
   MARK'(nil) -> c44
   A__TAKE''(0, z0) -> c51
   MARK'(s(z0)) -> c41
   A__TAKE'(s(z0), cons(z1, z2)) -> c30
   A__LENGTH''(z0) -> c56
   MARK''(cons(z0, z1)) -> c66
   A__LENGTH''(cons(z0, z1)) -> c55
   MARK'(0) -> c39
   A__EQ''(0, 0) -> c45
   MARK''(0) -> c62
   A__EQ''(z0, z1) -> c48
   A__EQ''(z0, z1) -> c47
   MARK''(false) -> c65
   MARK'(true) -> c40
   A__TAKE''(z0, z1) -> c53
   A__TAKE'(0, z0) -> c29
   A__INF''(z0) -> c49
   A__EQ'(z0, z1) -> c26
   A__LENGTH''(nil) -> c54
   A__LENGTH'(nil) -> c32
   A__INF'(z0) -> c27
   A__EQ'(z0, z1) -> c25
   A__LENGTH'(z0) -> c34

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil
   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22
Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   MARK'(inf(z0)) -> c36(A__INF'(mark(z0)), MARK'(z0))
   MARK'(take(z0, z1)) -> c37(A__TAKE'(mark(z0), mark(z1)), MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(A__LENGTH'(mark(z0)), MARK'(z0))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(A__INF''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(A__LENGTH''(mark(z0)), MARK'(z0), MARK''(z0))
S tuples:
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(A__INF''(mark(z0)), MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(A__TAKE''(mark(z0), mark(z1)), MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(A__LENGTH''(mark(z0)), MARK'(z0), MARK''(z0))
K tuples:none
Defined Rule Symbols:   A__EQ_2, A__INF_1, A__TAKE_2, A__LENGTH_1, MARK_1, a__eq_2, a__inf_1, a__take_2, a__length_1, mark_1

Defined Pair Symbols:   A__EQ'_2, MARK'_1, A__EQ''_2, MARK''_1

Compound Symbols:   c24_1, c35_1, c36_2, c37_3, c38_2, c46_1, c57_1, c58_3, c59_4, c60_4, c61_3


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil
   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22
Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
S tuples:
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
K tuples:none
Defined Rule Symbols:   A__EQ_2, A__INF_1, A__TAKE_2, A__LENGTH_1, MARK_1, a__eq_2, a__inf_1, a__take_2, a__length_1, mark_1

Defined Pair Symbols:   A__EQ'_2, MARK'_1, A__EQ''_2, MARK''_1

Compound Symbols:   c24_1, c35_1, c46_1, c57_1, c36_1, c37_2, c38_1, c58_2, c59_3, c60_3, c61_2


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   a__eq(0, 0) -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0, z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0) -> 0
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil
   A__EQ(0, 0) -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0, z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0) -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
S tuples:
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   A__EQ'_2, MARK'_1, A__EQ''_2, MARK''_1

Compound Symbols:   c24_1, c35_1, c46_1, c57_1, c36_1, c37_2, c38_1, c58_2, c59_3, c60_3, c61_2


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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(A__EQ'(x_1, x_2)) = 0
   POL(A__EQ''(x_1, x_2)) = [3] + [2]x_1 + [2]x_2
   POL(MARK'(x_1)) = 0
   POL(MARK''(x_1)) = [3] + [2]x_1
   POL(c24(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1, x_2)) = x_1 + x_2
   POL(c38(x_1)) = x_1
   POL(c46(x_1)) = x_1
   POL(c57(x_1)) = x_1
   POL(c58(x_1, x_2)) = x_1 + x_2
   POL(c59(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c60(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c61(x_1, x_2)) = x_1 + x_2
   POL(eq(x_1, x_2)) = [3] + x_1 + x_2
   POL(inf(x_1)) = [3] + x_1
   POL(length(x_1)) = [2] + x_1
   POL(s(x_1)) = [3] + x_1
   POL(take(x_1, x_2)) = x_1 + x_2

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
S tuples:
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
K tuples:
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   A__EQ'_2, MARK'_1, A__EQ''_2, MARK''_1

Compound Symbols:   c24_1, c35_1, c46_1, c57_1, c36_1, c37_2, c38_1, c58_2, c59_3, c60_3, c61_2


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
We considered the (Usable) Rules:none
And the Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(A__EQ'(x_1, x_2)) = 0
   POL(A__EQ''(x_1, x_2)) = x_1 + x_2
   POL(MARK'(x_1)) = 0
   POL(MARK''(x_1)) = [1] + x_1
   POL(c24(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1, x_2)) = x_1 + x_2
   POL(c38(x_1)) = x_1
   POL(c46(x_1)) = x_1
   POL(c57(x_1)) = x_1
   POL(c58(x_1, x_2)) = x_1 + x_2
   POL(c59(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c60(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c61(x_1, x_2)) = x_1 + x_2
   POL(eq(x_1, x_2)) = [1] + x_1 + x_2
   POL(inf(x_1)) = [1] + x_1
   POL(length(x_1)) = [1] + x_1
   POL(s(x_1)) = x_1
   POL(take(x_1, x_2)) = [1] + x_1 + x_2

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   A__EQ'(s(z0), s(z1)) -> c24(A__EQ'(z0, z1))
   MARK'(eq(z0, z1)) -> c35(A__EQ'(z0, z1))
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK'(inf(z0)) -> c36(MARK'(z0))
   MARK'(take(z0, z1)) -> c37(MARK'(z0), MARK'(z1))
   MARK'(length(z0)) -> c38(MARK'(z0))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
S tuples:none
K tuples:
   A__EQ''(s(z0), s(z1)) -> c46(A__EQ''(z0, z1))
   MARK''(eq(z0, z1)) -> c57(A__EQ''(z0, z1))
   MARK''(inf(z0)) -> c58(MARK'(z0), MARK''(z0))
   MARK''(length(z0)) -> c61(MARK'(z0), MARK''(z0))
   MARK''(take(z0, z1)) -> c59(MARK'(z0), MARK'(z1), MARK''(z0))
   MARK''(take(z0, z1)) -> c60(MARK'(z0), MARK'(z1), MARK''(z1))
Defined Rule Symbols:none

Defined Pair Symbols:   A__EQ'_2, MARK'_1, A__EQ''_2, MARK''_1

Compound Symbols:   c24_1, c35_1, c46_1, c57_1, c36_1, c37_2, c38_1, c58_2, c59_3, c60_3, c61_2


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

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

(16)
BOUNDS(1, 1)

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

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

(18)
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:

   A__EQ(0', 0') -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0', z0) -> c6
   A__TAKE(s(z0), cons(z1, z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z0, z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0') -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z0, z1)) -> c21
   MARK(nil) -> c22

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

   a__eq(0', 0') -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(z0, inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0', z0) -> nil
   a__take(s(z0), cons(z1, z2)) -> cons(z1, take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0'
   a__length(cons(z0, z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0') -> 0'
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z0, z1)) -> cons(z0, z1)
   mark(nil) -> nil

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

(19) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
cons/0

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

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

   A__EQ(0', 0') -> c
   A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
   A__EQ(z0, z1) -> c2
   A__EQ(z0, z1) -> c3
   A__INF(z0) -> c4
   A__INF(z0) -> c5
   A__TAKE(0', z0) -> c6
   A__TAKE(s(z0), cons(z2)) -> c7
   A__TAKE(z0, z1) -> c8
   A__LENGTH(nil) -> c9
   A__LENGTH(cons(z1)) -> c10
   A__LENGTH(z0) -> c11
   MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
   MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
   MARK(0') -> c17
   MARK(true) -> c18
   MARK(s(z0)) -> c19
   MARK(false) -> c20
   MARK(cons(z1)) -> c21
   MARK(nil) -> c22

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

   a__eq(0', 0') -> true
   a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
   a__eq(z0, z1) -> false
   a__eq(z0, z1) -> eq(z0, z1)
   a__inf(z0) -> cons(inf(s(z0)))
   a__inf(z0) -> inf(z0)
   a__take(0', z0) -> nil
   a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
   a__take(z0, z1) -> take(z0, z1)
   a__length(nil) -> 0'
   a__length(cons(z1)) -> s(length(z1))
   a__length(z0) -> length(z0)
   mark(eq(z0, z1)) -> a__eq(z0, z1)
   mark(inf(z0)) -> a__inf(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(length(z0)) -> a__length(mark(z0))
   mark(0') -> 0'
   mark(true) -> true
   mark(s(z0)) -> s(z0)
   mark(false) -> false
   mark(cons(z1)) -> cons(z1)
   mark(nil) -> nil

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

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

(22)
Obligation:
Innermost TRS:
Rules:
A__EQ(0', 0') -> c
A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
A__EQ(z0, z1) -> c2
A__EQ(z0, z1) -> c3
A__INF(z0) -> c4
A__INF(z0) -> c5
A__TAKE(0', z0) -> c6
A__TAKE(s(z0), cons(z2)) -> c7
A__TAKE(z0, z1) -> c8
A__LENGTH(nil) -> c9
A__LENGTH(cons(z1)) -> c10
A__LENGTH(z0) -> c11
MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
MARK(0') -> c17
MARK(true) -> c18
MARK(s(z0)) -> c19
MARK(false) -> c20
MARK(cons(z1)) -> c21
MARK(nil) -> c22
a__eq(0', 0') -> true
a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
a__eq(z0, z1) -> false
a__eq(z0, z1) -> eq(z0, z1)
a__inf(z0) -> cons(inf(s(z0)))
a__inf(z0) -> inf(z0)
a__take(0', z0) -> nil
a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
a__take(z0, z1) -> take(z0, z1)
a__length(nil) -> 0'
a__length(cons(z1)) -> s(length(z1))
a__length(z0) -> length(z0)
mark(eq(z0, z1)) -> a__eq(z0, z1)
mark(inf(z0)) -> a__inf(mark(z0))
mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
mark(length(z0)) -> a__length(mark(z0))
mark(0') -> 0'
mark(true) -> true
mark(s(z0)) -> s(z0)
mark(false) -> false
mark(cons(z1)) -> cons(z1)
mark(nil) -> nil

Types:
A__EQ :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c:c1:c2:c3
0' :: 0':s:cons:nil:eq:inf:take:length:true:false
c :: c:c1:c2:c3
s :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c1 :: c:c1:c2:c3 -> c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
A__INF :: 0':s:cons:nil:eq:inf:take:length:true:false -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
A__TAKE :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c6:c7:c8
c6 :: c6:c7:c8
cons :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__LENGTH :: 0':s:cons:nil:eq:inf:take:length:true:false -> c9:c10:c11
nil :: 0':s:cons:nil:eq:inf:take:length:true:false
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
MARK :: 0':s:cons:nil:eq:inf:take:length:true:false -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c12 :: c:c1:c2:c3 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c13 :: c4:c5 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
mark :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c14 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c15 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c16 :: c9:c10:c11 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c17 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
true :: 0':s:cons:nil:eq:inf:take:length:true:false
c18 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c19 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
false :: 0':s:cons:nil:eq:inf:take:length:true:false
c20 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c21 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c22 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
a__eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
hole_c:c1:c2:c31_23 :: c:c1:c2:c3
hole_0':s:cons:nil:eq:inf:take:length:true:false2_23 :: 0':s:cons:nil:eq:inf:take:length:true:false
hole_c4:c53_23 :: c4:c5
hole_c6:c7:c84_23 :: c6:c7:c8
hole_c9:c10:c115_23 :: c9:c10:c11
hole_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c226_23 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
gen_c:c1:c2:c37_23 :: Nat -> c:c1:c2:c3
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23 :: Nat -> 0':s:cons:nil:eq:inf:take:length:true:false
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23 :: Nat -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22

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

(23) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
A__EQ, MARK, mark, a__eq

They will be analysed ascendingly in the following order:
A__EQ < MARK
mark < MARK
a__eq < mark

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

(24)
Obligation:
Innermost TRS:
Rules:
A__EQ(0', 0') -> c
A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
A__EQ(z0, z1) -> c2
A__EQ(z0, z1) -> c3
A__INF(z0) -> c4
A__INF(z0) -> c5
A__TAKE(0', z0) -> c6
A__TAKE(s(z0), cons(z2)) -> c7
A__TAKE(z0, z1) -> c8
A__LENGTH(nil) -> c9
A__LENGTH(cons(z1)) -> c10
A__LENGTH(z0) -> c11
MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
MARK(0') -> c17
MARK(true) -> c18
MARK(s(z0)) -> c19
MARK(false) -> c20
MARK(cons(z1)) -> c21
MARK(nil) -> c22
a__eq(0', 0') -> true
a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
a__eq(z0, z1) -> false
a__eq(z0, z1) -> eq(z0, z1)
a__inf(z0) -> cons(inf(s(z0)))
a__inf(z0) -> inf(z0)
a__take(0', z0) -> nil
a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
a__take(z0, z1) -> take(z0, z1)
a__length(nil) -> 0'
a__length(cons(z1)) -> s(length(z1))
a__length(z0) -> length(z0)
mark(eq(z0, z1)) -> a__eq(z0, z1)
mark(inf(z0)) -> a__inf(mark(z0))
mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
mark(length(z0)) -> a__length(mark(z0))
mark(0') -> 0'
mark(true) -> true
mark(s(z0)) -> s(z0)
mark(false) -> false
mark(cons(z1)) -> cons(z1)
mark(nil) -> nil

Types:
A__EQ :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c:c1:c2:c3
0' :: 0':s:cons:nil:eq:inf:take:length:true:false
c :: c:c1:c2:c3
s :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c1 :: c:c1:c2:c3 -> c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
A__INF :: 0':s:cons:nil:eq:inf:take:length:true:false -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
A__TAKE :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c6:c7:c8
c6 :: c6:c7:c8
cons :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__LENGTH :: 0':s:cons:nil:eq:inf:take:length:true:false -> c9:c10:c11
nil :: 0':s:cons:nil:eq:inf:take:length:true:false
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
MARK :: 0':s:cons:nil:eq:inf:take:length:true:false -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c12 :: c:c1:c2:c3 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c13 :: c4:c5 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
mark :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c14 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c15 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c16 :: c9:c10:c11 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c17 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
true :: 0':s:cons:nil:eq:inf:take:length:true:false
c18 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c19 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
false :: 0':s:cons:nil:eq:inf:take:length:true:false
c20 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c21 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c22 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
a__eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
hole_c:c1:c2:c31_23 :: c:c1:c2:c3
hole_0':s:cons:nil:eq:inf:take:length:true:false2_23 :: 0':s:cons:nil:eq:inf:take:length:true:false
hole_c4:c53_23 :: c4:c5
hole_c6:c7:c84_23 :: c6:c7:c8
hole_c9:c10:c115_23 :: c9:c10:c11
hole_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c226_23 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
gen_c:c1:c2:c37_23 :: Nat -> c:c1:c2:c3
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23 :: Nat -> 0':s:cons:nil:eq:inf:take:length:true:false
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23 :: Nat -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22


Generator Equations:
gen_c:c1:c2:c37_23(0) <=> c
gen_c:c1:c2:c37_23(+(x, 1)) <=> c1(gen_c:c1:c2:c37_23(x))
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0) <=> 0'
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(x, 1)) <=> s(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(x))
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(0) <=> c12(c)
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(+(x, 1)) <=> c13(c4, gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(x))


The following defined symbols remain to be analysed:
A__EQ, MARK, mark, a__eq

They will be analysed ascendingly in the following order:
A__EQ < MARK
mark < MARK
a__eq < mark

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23)) -> gen_c:c1:c2:c37_23(n11_23), rt in Omega(1 + n11_23)

Induction Base:
A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0)) ->_R^Omega(1)
c

Induction Step:
A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(n11_23, 1)), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(n11_23, 1))) ->_R^Omega(1)
c1(A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23))) ->_IH
c1(gen_c:c1:c2:c37_23(c12_23))

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

(26)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
A__EQ(0', 0') -> c
A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
A__EQ(z0, z1) -> c2
A__EQ(z0, z1) -> c3
A__INF(z0) -> c4
A__INF(z0) -> c5
A__TAKE(0', z0) -> c6
A__TAKE(s(z0), cons(z2)) -> c7
A__TAKE(z0, z1) -> c8
A__LENGTH(nil) -> c9
A__LENGTH(cons(z1)) -> c10
A__LENGTH(z0) -> c11
MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
MARK(0') -> c17
MARK(true) -> c18
MARK(s(z0)) -> c19
MARK(false) -> c20
MARK(cons(z1)) -> c21
MARK(nil) -> c22
a__eq(0', 0') -> true
a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
a__eq(z0, z1) -> false
a__eq(z0, z1) -> eq(z0, z1)
a__inf(z0) -> cons(inf(s(z0)))
a__inf(z0) -> inf(z0)
a__take(0', z0) -> nil
a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
a__take(z0, z1) -> take(z0, z1)
a__length(nil) -> 0'
a__length(cons(z1)) -> s(length(z1))
a__length(z0) -> length(z0)
mark(eq(z0, z1)) -> a__eq(z0, z1)
mark(inf(z0)) -> a__inf(mark(z0))
mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
mark(length(z0)) -> a__length(mark(z0))
mark(0') -> 0'
mark(true) -> true
mark(s(z0)) -> s(z0)
mark(false) -> false
mark(cons(z1)) -> cons(z1)
mark(nil) -> nil

Types:
A__EQ :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c:c1:c2:c3
0' :: 0':s:cons:nil:eq:inf:take:length:true:false
c :: c:c1:c2:c3
s :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c1 :: c:c1:c2:c3 -> c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
A__INF :: 0':s:cons:nil:eq:inf:take:length:true:false -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
A__TAKE :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c6:c7:c8
c6 :: c6:c7:c8
cons :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__LENGTH :: 0':s:cons:nil:eq:inf:take:length:true:false -> c9:c10:c11
nil :: 0':s:cons:nil:eq:inf:take:length:true:false
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
MARK :: 0':s:cons:nil:eq:inf:take:length:true:false -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c12 :: c:c1:c2:c3 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c13 :: c4:c5 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
mark :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c14 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c15 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c16 :: c9:c10:c11 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c17 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
true :: 0':s:cons:nil:eq:inf:take:length:true:false
c18 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c19 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
false :: 0':s:cons:nil:eq:inf:take:length:true:false
c20 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c21 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c22 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
a__eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
hole_c:c1:c2:c31_23 :: c:c1:c2:c3
hole_0':s:cons:nil:eq:inf:take:length:true:false2_23 :: 0':s:cons:nil:eq:inf:take:length:true:false
hole_c4:c53_23 :: c4:c5
hole_c6:c7:c84_23 :: c6:c7:c8
hole_c9:c10:c115_23 :: c9:c10:c11
hole_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c226_23 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
gen_c:c1:c2:c37_23 :: Nat -> c:c1:c2:c3
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23 :: Nat -> 0':s:cons:nil:eq:inf:take:length:true:false
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23 :: Nat -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22


Generator Equations:
gen_c:c1:c2:c37_23(0) <=> c
gen_c:c1:c2:c37_23(+(x, 1)) <=> c1(gen_c:c1:c2:c37_23(x))
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0) <=> 0'
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(x, 1)) <=> s(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(x))
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(0) <=> c12(c)
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(+(x, 1)) <=> c13(c4, gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(x))


The following defined symbols remain to be analysed:
A__EQ, MARK, mark, a__eq

They will be analysed ascendingly in the following order:
A__EQ < MARK
mark < MARK
a__eq < mark

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

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

(29)
BOUNDS(n^1, INF)

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

(30)
Obligation:
Innermost TRS:
Rules:
A__EQ(0', 0') -> c
A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
A__EQ(z0, z1) -> c2
A__EQ(z0, z1) -> c3
A__INF(z0) -> c4
A__INF(z0) -> c5
A__TAKE(0', z0) -> c6
A__TAKE(s(z0), cons(z2)) -> c7
A__TAKE(z0, z1) -> c8
A__LENGTH(nil) -> c9
A__LENGTH(cons(z1)) -> c10
A__LENGTH(z0) -> c11
MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
MARK(0') -> c17
MARK(true) -> c18
MARK(s(z0)) -> c19
MARK(false) -> c20
MARK(cons(z1)) -> c21
MARK(nil) -> c22
a__eq(0', 0') -> true
a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
a__eq(z0, z1) -> false
a__eq(z0, z1) -> eq(z0, z1)
a__inf(z0) -> cons(inf(s(z0)))
a__inf(z0) -> inf(z0)
a__take(0', z0) -> nil
a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
a__take(z0, z1) -> take(z0, z1)
a__length(nil) -> 0'
a__length(cons(z1)) -> s(length(z1))
a__length(z0) -> length(z0)
mark(eq(z0, z1)) -> a__eq(z0, z1)
mark(inf(z0)) -> a__inf(mark(z0))
mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
mark(length(z0)) -> a__length(mark(z0))
mark(0') -> 0'
mark(true) -> true
mark(s(z0)) -> s(z0)
mark(false) -> false
mark(cons(z1)) -> cons(z1)
mark(nil) -> nil

Types:
A__EQ :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c:c1:c2:c3
0' :: 0':s:cons:nil:eq:inf:take:length:true:false
c :: c:c1:c2:c3
s :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c1 :: c:c1:c2:c3 -> c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
A__INF :: 0':s:cons:nil:eq:inf:take:length:true:false -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
A__TAKE :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c6:c7:c8
c6 :: c6:c7:c8
cons :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__LENGTH :: 0':s:cons:nil:eq:inf:take:length:true:false -> c9:c10:c11
nil :: 0':s:cons:nil:eq:inf:take:length:true:false
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
MARK :: 0':s:cons:nil:eq:inf:take:length:true:false -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c12 :: c:c1:c2:c3 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c13 :: c4:c5 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
mark :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c14 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c15 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c16 :: c9:c10:c11 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c17 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
true :: 0':s:cons:nil:eq:inf:take:length:true:false
c18 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c19 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
false :: 0':s:cons:nil:eq:inf:take:length:true:false
c20 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c21 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c22 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
a__eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
hole_c:c1:c2:c31_23 :: c:c1:c2:c3
hole_0':s:cons:nil:eq:inf:take:length:true:false2_23 :: 0':s:cons:nil:eq:inf:take:length:true:false
hole_c4:c53_23 :: c4:c5
hole_c6:c7:c84_23 :: c6:c7:c8
hole_c9:c10:c115_23 :: c9:c10:c11
hole_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c226_23 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
gen_c:c1:c2:c37_23 :: Nat -> c:c1:c2:c3
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23 :: Nat -> 0':s:cons:nil:eq:inf:take:length:true:false
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23 :: Nat -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22


Lemmas:
A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23)) -> gen_c:c1:c2:c37_23(n11_23), rt in Omega(1 + n11_23)


Generator Equations:
gen_c:c1:c2:c37_23(0) <=> c
gen_c:c1:c2:c37_23(+(x, 1)) <=> c1(gen_c:c1:c2:c37_23(x))
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0) <=> 0'
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(x, 1)) <=> s(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(x))
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(0) <=> c12(c)
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(+(x, 1)) <=> c13(c4, gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(x))


The following defined symbols remain to be analysed:
a__eq, MARK, mark

They will be analysed ascendingly in the following order:
mark < MARK
a__eq < mark

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
a__eq(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23)) -> true, rt in Omega(0)

Induction Base:
a__eq(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0)) ->_R^Omega(0)
true

Induction Step:
a__eq(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(n807_23, 1)), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(n807_23, 1))) ->_R^Omega(0)
a__eq(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23)) ->_IH
true

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

(32)
Obligation:
Innermost TRS:
Rules:
A__EQ(0', 0') -> c
A__EQ(s(z0), s(z1)) -> c1(A__EQ(z0, z1))
A__EQ(z0, z1) -> c2
A__EQ(z0, z1) -> c3
A__INF(z0) -> c4
A__INF(z0) -> c5
A__TAKE(0', z0) -> c6
A__TAKE(s(z0), cons(z2)) -> c7
A__TAKE(z0, z1) -> c8
A__LENGTH(nil) -> c9
A__LENGTH(cons(z1)) -> c10
A__LENGTH(z0) -> c11
MARK(eq(z0, z1)) -> c12(A__EQ(z0, z1))
MARK(inf(z0)) -> c13(A__INF(mark(z0)), MARK(z0))
MARK(take(z0, z1)) -> c14(A__TAKE(mark(z0), mark(z1)), MARK(z0))
MARK(take(z0, z1)) -> c15(A__TAKE(mark(z0), mark(z1)), MARK(z1))
MARK(length(z0)) -> c16(A__LENGTH(mark(z0)), MARK(z0))
MARK(0') -> c17
MARK(true) -> c18
MARK(s(z0)) -> c19
MARK(false) -> c20
MARK(cons(z1)) -> c21
MARK(nil) -> c22
a__eq(0', 0') -> true
a__eq(s(z0), s(z1)) -> a__eq(z0, z1)
a__eq(z0, z1) -> false
a__eq(z0, z1) -> eq(z0, z1)
a__inf(z0) -> cons(inf(s(z0)))
a__inf(z0) -> inf(z0)
a__take(0', z0) -> nil
a__take(s(z0), cons(z2)) -> cons(take(z0, z2))
a__take(z0, z1) -> take(z0, z1)
a__length(nil) -> 0'
a__length(cons(z1)) -> s(length(z1))
a__length(z0) -> length(z0)
mark(eq(z0, z1)) -> a__eq(z0, z1)
mark(inf(z0)) -> a__inf(mark(z0))
mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
mark(length(z0)) -> a__length(mark(z0))
mark(0') -> 0'
mark(true) -> true
mark(s(z0)) -> s(z0)
mark(false) -> false
mark(cons(z1)) -> cons(z1)
mark(nil) -> nil

Types:
A__EQ :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c:c1:c2:c3
0' :: 0':s:cons:nil:eq:inf:take:length:true:false
c :: c:c1:c2:c3
s :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c1 :: c:c1:c2:c3 -> c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
A__INF :: 0':s:cons:nil:eq:inf:take:length:true:false -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
A__TAKE :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> c6:c7:c8
c6 :: c6:c7:c8
cons :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__LENGTH :: 0':s:cons:nil:eq:inf:take:length:true:false -> c9:c10:c11
nil :: 0':s:cons:nil:eq:inf:take:length:true:false
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
MARK :: 0':s:cons:nil:eq:inf:take:length:true:false -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c12 :: c:c1:c2:c3 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c13 :: c4:c5 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
mark :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c14 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c15 :: c6:c7:c8 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
c16 :: c9:c10:c11 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22 -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c17 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
true :: 0':s:cons:nil:eq:inf:take:length:true:false
c18 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c19 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
false :: 0':s:cons:nil:eq:inf:take:length:true:false
c20 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c21 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
c22 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
a__eq :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__inf :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__take :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
a__length :: 0':s:cons:nil:eq:inf:take:length:true:false -> 0':s:cons:nil:eq:inf:take:length:true:false
hole_c:c1:c2:c31_23 :: c:c1:c2:c3
hole_0':s:cons:nil:eq:inf:take:length:true:false2_23 :: 0':s:cons:nil:eq:inf:take:length:true:false
hole_c4:c53_23 :: c4:c5
hole_c6:c7:c84_23 :: c6:c7:c8
hole_c9:c10:c115_23 :: c9:c10:c11
hole_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c226_23 :: c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22
gen_c:c1:c2:c37_23 :: Nat -> c:c1:c2:c3
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23 :: Nat -> 0':s:cons:nil:eq:inf:take:length:true:false
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23 :: Nat -> c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c22


Lemmas:
A__EQ(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n11_23)) -> gen_c:c1:c2:c37_23(n11_23), rt in Omega(1 + n11_23)
a__eq(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23), gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(n807_23)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c37_23(0) <=> c
gen_c:c1:c2:c37_23(+(x, 1)) <=> c1(gen_c:c1:c2:c37_23(x))
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(0) <=> 0'
gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(+(x, 1)) <=> s(gen_0':s:cons:nil:eq:inf:take:length:true:false8_23(x))
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(0) <=> c12(c)
gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(+(x, 1)) <=> c13(c4, gen_c12:c13:c14:c15:c16:c17:c18:c19:c20:c21:c229_23(x))


The following defined symbols remain to be analysed:
mark, MARK

They will be analysed ascendingly in the following order:
mark < MARK