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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (8) CdtProblem
    (9) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CdtProblem
    (13) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxRelTRS
    (15) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxWeightedTrs
    (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxTypedWeightedTrs
    (19) CompletionProof [UPPER BOUND(ID), 0 ms]
    (20) CpxTypedWeightedCompleteTrs
    (21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (22) CpxRNTS
    (23) CompleteCoflocoProof [FINISHED, 1271 ms]
    (24) BOUNDS(1, n^2)
(25) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(26) CdtProblem
    (27) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) CpxRelTRS
    (29) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) CpxRelTRS
    (31) TypeInferenceProof [BOTH BOUNDS(ID, ID), 7 ms]
    (32) typed CpxTrs
    (33) OrderProof [LOWER BOUND(ID), 0 ms]
    (34) typed CpxTrs
    (35) RewriteLemmaProof [LOWER BOUND(ID), 311 ms]
    (36) typed CpxTrs
    (37) RewriteLemmaProof [LOWER BOUND(ID), 55 ms]
    (38) typed CpxTrs
    (39) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
    (40) BEST
        (41) proven lower bound
            (42) LowerBoundPropagationProof [FINISHED, 0 ms]
            (43) BOUNDS(n^1, INF)
        (44) typed CpxTrs
            (45) RewriteLemmaProof [LOWER BOUND(ID), 59 ms]
            (46) typed CpxTrs
            (47) RewriteLemmaProof [LOWER BOUND(ID), 40 ms]
            (48) typed CpxTrs
            (49) RewriteLemmaProof [LOWER BOUND(ID), 88 ms]
            (50) typed CpxTrs
            (51) RewriteLemmaProof [LOWER BOUND(ID), 3218 ms]
            (52) typed CpxTrs
            (53) RewriteLemmaProof [LOWER BOUND(ID), 35 ms]
            (54) typed CpxTrs


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

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


The TRS R consists of the following rules:

   app(x, y) -> helpa(0, plus(length(x), length(y)), x, y)
   plus(x, 0) -> x
   plus(x, s(y)) -> s(plus(x, y))
   length(nil) -> 0
   length(cons(x, y)) -> s(length(y))
   helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if(true, c, l, ys, zs) -> nil
   if(false, c, l, ys, zs) -> helpb(c, l, ys, zs)
   take(0, cons(x, xs), ys) -> x
   take(0, nil, cons(y, ys)) -> y
   take(s(c), cons(x, xs), ys) -> take(c, xs, ys)
   take(s(c), nil, cons(y, ys)) -> take(c, nil, ys)
   helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0) -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0) -> c7
   GE(0, s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0, cons(z0, xs), z1) -> c12
   TAKE(0, nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
S tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0) -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0) -> c7
   GE(0, s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0, cons(z0, xs), z1) -> c12
   TAKE(0, nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
K tuples:none
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   APP_2, PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4

Compound Symbols:   c_3, c1_3, c2, c3_1, c4, c5_1, c6_2, c7, c8, c9_1, c10, c11_1, c12, c13, c14_1, c15_1, c16_1, c17_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   TAKE(0, nil, cons(z0, z1)) -> c13
   GE(z0, 0) -> c7
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   PLUS(z0, 0) -> c2
   GE(0, s(z0)) -> c8
   LENGTH(nil) -> c4
   TAKE(0, cons(z0, xs), z1) -> c12
   IF(true, z0, z1, z2, z3) -> c10

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
S tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
K tuples:none
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   APP_2, PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4

Compound Symbols:   c_3, c1_3, c3_1, c5_1, c6_2, c9_1, c11_1, c15_1, c16_1, c17_1


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
   APP(z0, z1) -> c2(LENGTH(z0))
   APP(z0, z1) -> c2(LENGTH(z1))
S tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
   APP(z0, z1) -> c2(LENGTH(z0))
   APP(z0, z1) -> c2(LENGTH(z1))
K tuples:none
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4, APP_2

Compound Symbols:   c3_1, c5_1, c6_2, c9_1, c11_1, c15_1, c16_1, c17_1, c2_1


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

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   APP(z0, z1) -> c2(LENGTH(z0))
   APP(z0, z1) -> c2(LENGTH(z1))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
S tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
K tuples:none
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4, APP_2

Compound Symbols:   c3_1, c5_1, c6_2, c9_1, c11_1, c15_1, c16_1, c17_1, c2_1


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

(9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
S tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
K tuples:
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4, APP_2

Compound Symbols:   c3_1, c5_1, c6_2, c9_1, c11_1, c15_1, c16_1, c17_1, c2_1


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

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
Tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
S tuples:
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
K tuples:
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
Defined Rule Symbols:   ge_2, plus_2, length_1

Defined Pair Symbols:   PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4, APP_2

Compound Symbols:   c3_1, c5_1, c6_2, c9_1, c11_1, c15_1, c16_1, c17_1, c2_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 CpxRelTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))

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

   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1))
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))

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

(15) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1]
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1]
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1]
   GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1]
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1]
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1]
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1]
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1]
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1)) [0]
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1))) [0]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]

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

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

(18)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1]
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1]
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1]
   GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1]
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1]
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1]
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1]
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1]
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1)) [0]
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1))) [0]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]

The TRS has the following type information:
PLUS :: s:0 -> s:0 -> c3:c6
s :: s:0 -> s:0
c3 :: c3:c6 -> c3:c6
LENGTH :: cons:nil -> c5
cons :: a -> cons:nil -> cons:nil
c5 :: c5 -> c5
HELPA :: s:0 -> s:0 -> cons:nil -> cons:nil -> c3:c6
c6 :: c11 -> c9 -> c3:c6
IF :: false:true -> s:0 -> s:0 -> cons:nil -> cons:nil -> c11
ge :: s:0 -> s:0 -> false:true
GE :: s:0 -> s:0 -> c9
c9 :: c9 -> c9
false :: false:true
c11 :: c16:c17 -> c11
HELPB :: s:0 -> s:0 -> cons:nil -> cons:nil -> c16:c17
TAKE :: s:0 -> cons:nil -> cons:nil -> c15
nil :: cons:nil
c15 :: c15 -> c15
c16 :: c15 -> c16:c17
c17 :: c3:c6 -> c16:c17
APP :: cons:nil -> cons:nil -> c2
c2 :: c3:c6 -> c2
0 :: s:0
plus :: s:0 -> s:0 -> s:0
length :: cons:nil -> s:0
true :: false:true

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

(19) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   APP(v0, v1) -> null_APP [0]
   ge(v0, v1) -> null_ge [0]
   plus(v0, v1) -> null_plus [0]
   length(v0) -> null_length [0]
   PLUS(v0, v1) -> null_PLUS [0]
   LENGTH(v0) -> null_LENGTH [0]
   GE(v0, v1) -> null_GE [0]
   IF(v0, v1, v2, v3, v4) -> null_IF [0]
   TAKE(v0, v1, v2) -> null_TAKE [0]

And the following fresh constants:    null_APP, null_ge, null_plus, null_length, null_PLUS, null_LENGTH, null_GE, null_IF, null_TAKE, const, const1

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

(20)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1]
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1]
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1]
   GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1]
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1]
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1]
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1]
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1]
   APP(z0, z1) -> c2(HELPA(0, plus(length(z0), length(z1)), z0, z1)) [0]
   APP(z0, z1) -> c2(PLUS(length(z0), length(z1))) [0]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]
   APP(v0, v1) -> null_APP [0]
   ge(v0, v1) -> null_ge [0]
   plus(v0, v1) -> null_plus [0]
   length(v0) -> null_length [0]
   PLUS(v0, v1) -> null_PLUS [0]
   LENGTH(v0) -> null_LENGTH [0]
   GE(v0, v1) -> null_GE [0]
   IF(v0, v1, v2, v3, v4) -> null_IF [0]
   TAKE(v0, v1, v2) -> null_TAKE [0]

The TRS has the following type information:
PLUS :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> c3:c6:null_PLUS
s :: s:0:null_plus:null_length -> s:0:null_plus:null_length
c3 :: c3:c6:null_PLUS -> c3:c6:null_PLUS
LENGTH :: cons:nil -> c5:null_LENGTH
cons :: a -> cons:nil -> cons:nil
c5 :: c5:null_LENGTH -> c5:null_LENGTH
HELPA :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> cons:nil -> cons:nil -> c3:c6:null_PLUS
c6 :: c11:null_IF -> c9:null_GE -> c3:c6:null_PLUS
IF :: false:true:null_ge -> s:0:null_plus:null_length -> s:0:null_plus:null_length -> cons:nil -> cons:nil -> c11:null_IF
ge :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> false:true:null_ge
GE :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> c9:null_GE
c9 :: c9:null_GE -> c9:null_GE
false :: false:true:null_ge
c11 :: c16:c17 -> c11:null_IF
HELPB :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> cons:nil -> cons:nil -> c16:c17
TAKE :: s:0:null_plus:null_length -> cons:nil -> cons:nil -> c15:null_TAKE
nil :: cons:nil
c15 :: c15:null_TAKE -> c15:null_TAKE
c16 :: c15:null_TAKE -> c16:c17
c17 :: c3:c6:null_PLUS -> c16:c17
APP :: cons:nil -> cons:nil -> c2:null_APP
c2 :: c3:c6:null_PLUS -> c2:null_APP
0 :: s:0:null_plus:null_length
plus :: s:0:null_plus:null_length -> s:0:null_plus:null_length -> s:0:null_plus:null_length
length :: cons:nil -> s:0:null_plus:null_length
true :: false:true:null_ge
null_APP :: c2:null_APP
null_ge :: false:true:null_ge
null_plus :: s:0:null_plus:null_length
null_length :: s:0:null_plus:null_length
null_PLUS :: c3:c6:null_PLUS
null_LENGTH :: c5:null_LENGTH
null_GE :: c9:null_GE
null_IF :: c11:null_IF
null_TAKE :: c15:null_TAKE
const :: a
const1 :: c16:c17

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

(21) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   false => 1
   nil => 0
   0 => 0
   true => 2
   null_APP => 0
   null_ge => 0
   null_plus => 0
   null_length => 0
   null_PLUS => 0
   null_LENGTH => 0
   null_GE => 0
   null_IF => 0
   null_TAKE => 0
   const => 0
   const1 => 0

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

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   APP(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   APP(z, z') -{ 0 }-> 1 + PLUS(length(z0), length(z1)) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   APP(z, z') -{ 0 }-> 1 + HELPA(0, plus(length(z0), length(z1)), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   GE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   GE(z, z') -{ 1 }-> 1 + GE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   HELPA(z, z', z'', z4) -{ 1 }-> 1 + IF(ge(z0, z1), z0, z1, z2, z3) + GE(z0, z1) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0
   HELPB(z, z', z'', z4) -{ 1 }-> 1 + TAKE(z0, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0
   HELPB(z, z', z'', z4) -{ 1 }-> 1 + HELPA(1 + z0, z1, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0
   IF(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0
   IF(z, z', z'', z4, z5) -{ 1 }-> 1 + HELPB(z0, z1, z2, z3) :|: z1 >= 0, z = 1, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2
   LENGTH(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   LENGTH(z) -{ 1 }-> 1 + LENGTH(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   PLUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   PLUS(z, z') -{ 1 }-> 1 + PLUS(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   TAKE(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   TAKE(z, z', z'') -{ 1 }-> 1 + TAKE(z0, 0, z2) :|: z1 >= 0, z'' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0
   ge(z, z') -{ 0 }-> ge(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   ge(z, z') -{ 0 }-> 2 :|: z = z0, z0 >= 0, z' = 0
   ge(z, z') -{ 0 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0
   ge(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   length(z) -{ 0 }-> 0 :|: z = 0
   length(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   length(z) -{ 0 }-> 1 + length(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   plus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + plus(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1

Only complete derivations are relevant for the runtime complexity.

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

(23) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V, V7, V6, V16),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun1(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun2(V1, V, V7, V6, Out)],[V1 >= 0,V >= 0,V7 >= 0,V6 >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun3(V1, V, V7, V6, V16, Out)],[V1 >= 0,V >= 0,V7 >= 0,V6 >= 0,V16 >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun6(V1, V, V7, Out)],[V1 >= 0,V >= 0,V7 >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun5(V1, V, V7, V6, Out)],[V1 >= 0,V >= 0,V7 >= 0,V6 >= 0]).
eq(start(V1, V, V7, V6, V16),0,[fun7(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7, V6, V16),0,[ge(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7, V6, V16),0,[plus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7, V6, V16),0,[length(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V1 = V3,V2 >= 0,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, Out),1,[fun1(V4, Ret11)],[Out = 1 + Ret11,V4 >= 0,V5 >= 0,V1 = 1 + V4 + V5]).
eq(fun2(V1, V, V7, V6, Out),1,[ge(V9, V8, Ret010),fun3(Ret010, V9, V8, V11, V10, Ret01),fun4(V9, V8, Ret12)],[Out = 1 + Ret01 + Ret12,V7 = V11,V1 = V9,V8 >= 0,V = V8,V9 >= 0,V6 = V10,V11 >= 0,V10 >= 0]).
eq(fun4(V1, V, Out),1,[fun4(V12, V13, Ret13)],[Out = 1 + Ret13,V13 >= 0,V1 = 1 + V12,V12 >= 0,V = 1 + V13]).
eq(fun3(V1, V, V7, V6, V16, Out),1,[fun5(V15, V14, V17, V18, Ret14)],[Out = 1 + Ret14,V14 >= 0,V1 = 1,V15 >= 0,V16 = V18,V = V15,V17 >= 0,V18 >= 0,V7 = V14,V6 = V17]).
eq(fun6(V1, V, V7, Out),1,[fun6(V20, 0, V21, Ret15)],[Out = 1 + Ret15,V19 >= 0,V7 = 1 + V19 + V21,V1 = 1 + V20,V20 >= 0,V21 >= 0,V = 0]).
eq(fun5(V1, V, V7, V6, Out),1,[fun6(V23, V25, V24, Ret16)],[Out = 1 + Ret16,V7 = V25,V1 = V23,V22 >= 0,V = V22,V23 >= 0,V6 = V24,V25 >= 0,V24 >= 0]).
eq(fun5(V1, V, V7, V6, Out),1,[fun2(1 + V29, V26, V28, V27, Ret17)],[Out = 1 + Ret17,V7 = V28,V1 = V29,V26 >= 0,V = V26,V29 >= 0,V6 = V27,V28 >= 0,V27 >= 0]).
eq(fun7(V1, V, Out),0,[length(V31, Ret110),length(V30, Ret111),plus(Ret110, Ret111, Ret112),fun2(0, Ret112, V31, V30, Ret18)],[Out = 1 + Ret18,V1 = V31,V30 >= 0,V = V30,V31 >= 0]).
eq(fun7(V1, V, Out),0,[length(V32, Ret10),length(V33, Ret113),fun(Ret10, Ret113, Ret19)],[Out = 1 + Ret19,V1 = V32,V33 >= 0,V = V33,V32 >= 0]).
eq(ge(V1, V, Out),0,[],[Out = 2,V1 = V34,V34 >= 0,V = 0]).
eq(ge(V1, V, Out),0,[],[Out = 1,V35 >= 0,V = 1 + V35,V1 = 0]).
eq(ge(V1, V, Out),0,[ge(V36, V37, Ret)],[Out = Ret,V37 >= 0,V1 = 1 + V36,V36 >= 0,V = 1 + V37]).
eq(plus(V1, V, Out),0,[],[Out = V38,V1 = V38,V38 >= 0,V = 0]).
eq(plus(V1, V, Out),0,[plus(V40, V39, Ret114)],[Out = 1 + Ret114,V1 = V40,V39 >= 0,V40 >= 0,V = 1 + V39]).
eq(length(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(length(V1, Out),0,[length(V41, Ret115)],[Out = 1 + Ret115,V41 >= 0,V42 >= 0,V1 = 1 + V41 + V42]).
eq(fun7(V1, V, Out),0,[],[Out = 0,V44 >= 0,V43 >= 0,V1 = V44,V = V43]).
eq(ge(V1, V, Out),0,[],[Out = 0,V46 >= 0,V45 >= 0,V1 = V46,V = V45]).
eq(plus(V1, V, Out),0,[],[Out = 0,V48 >= 0,V47 >= 0,V1 = V48,V = V47]).
eq(length(V1, Out),0,[],[Out = 0,V49 >= 0,V1 = V49]).
eq(fun(V1, V, Out),0,[],[Out = 0,V50 >= 0,V51 >= 0,V1 = V50,V = V51]).
eq(fun1(V1, Out),0,[],[Out = 0,V52 >= 0,V1 = V52]).
eq(fun4(V1, V, Out),0,[],[Out = 0,V54 >= 0,V53 >= 0,V1 = V54,V = V53]).
eq(fun3(V1, V, V7, V6, V16, Out),0,[],[Out = 0,V16 = V57,V55 >= 0,V57 >= 0,V7 = V59,V56 >= 0,V1 = V55,V = V56,V6 = V58,V59 >= 0,V58 >= 0]).
eq(fun6(V1, V, V7, Out),0,[],[Out = 0,V60 >= 0,V7 = V62,V61 >= 0,V1 = V60,V = V61,V62 >= 0]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,Out),[V1],[Out]).
input_output_vars(fun2(V1,V,V7,V6,Out),[V1,V,V7,V6],[Out]).
input_output_vars(fun4(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun3(V1,V,V7,V6,V16,Out),[V1,V,V7,V6,V16],[Out]).
input_output_vars(fun6(V1,V,V7,Out),[V1,V,V7],[Out]).
input_output_vars(fun5(V1,V,V7,V6,Out),[V1,V,V7,V6],[Out]).
input_output_vars(fun7(V1,V,Out),[V1,V],[Out]).
input_output_vars(ge(V1,V,Out),[V1,V],[Out]).
input_output_vars(plus(V1,V,Out),[V1,V],[Out]).
input_output_vars(length(V1,Out),[V1],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [fun/3]
1. recursive  : [fun1/2]
2. recursive  : [fun6/4]
3. recursive  : [fun4/3]
4. recursive  : [ge/3]
5. recursive [non_tail] : [fun2/5,fun3/6,fun5/5]
6. recursive  : [length/2]
7. recursive  : [plus/3]
8. non_recursive  : [fun7/3]
9. non_recursive  : [start/5]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into fun1/2
2. SCC is partially evaluated into fun6/4
3. SCC is partially evaluated into fun4/3
4. SCC is partially evaluated into ge/3
5. SCC is partially evaluated into fun2/5
6. SCC is partially evaluated into length/2
7. SCC is partially evaluated into plus/3
8. SCC is partially evaluated into fun7/3
9. SCC is partially evaluated into start/5

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun/3 
* CE 21 is refined into CE [38] 
* CE 20 is refined into CE [39] 


### Cost equations --> "Loop" of fun/3 
* CEs [39] --> Loop 22 
* CEs [38] --> Loop 23 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [22]: [V]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [22]:
  - RF of loop [22:1]:
    V


### Specialization of cost equations fun1/2 
* CE 23 is refined into CE [40] 
* CE 22 is refined into CE [41] 


### Cost equations --> "Loop" of fun1/2 
* CEs [41] --> Loop 24 
* CEs [40] --> Loop 25 

### Ranking functions of CR fun1(V1,Out) 
* RF of phase [24]: [V1]

#### Partial ranking functions of CR fun1(V1,Out) 
* Partial RF of phase [24]:
  - RF of loop [24:1]:
    V1


### Specialization of cost equations fun6/4 
* CE 16 is refined into CE [42] 
* CE 15 is refined into CE [43] 


### Cost equations --> "Loop" of fun6/4 
* CEs [43] --> Loop 26 
* CEs [42] --> Loop 27 

### Ranking functions of CR fun6(V1,V,V7,Out) 
* RF of phase [26]: [V1,V7]

#### Partial ranking functions of CR fun6(V1,V,V7,Out) 
* Partial RF of phase [26]:
  - RF of loop [26:1]:
    V1
    V7


### Specialization of cost equations fun4/3 
* CE 25 is refined into CE [44] 
* CE 24 is refined into CE [45] 


### Cost equations --> "Loop" of fun4/3 
* CEs [45] --> Loop 28 
* CEs [44] --> Loop 29 

### Ranking functions of CR fun4(V1,V,Out) 
* RF of phase [28]: [V,V1]

#### Partial ranking functions of CR fun4(V1,V,Out) 
* Partial RF of phase [28]:
  - RF of loop [28:1]:
    V
    V1


### Specialization of cost equations ge/3 
* CE 32 is refined into CE [46] 
* CE 29 is refined into CE [47] 
* CE 30 is refined into CE [48] 
* CE 31 is refined into CE [49] 


### Cost equations --> "Loop" of ge/3 
* CEs [49] --> Loop 30 
* CEs [46] --> Loop 31 
* CEs [47] --> Loop 32 
* CEs [48] --> Loop 33 

### Ranking functions of CR ge(V1,V,Out) 
* RF of phase [30]: [V,V1]

#### Partial ranking functions of CR ge(V1,V,Out) 
* Partial RF of phase [30]:
  - RF of loop [30:1]:
    V
    V1


### Specialization of cost equations fun2/5 
* CE 19 is refined into CE [50,51,52] 
* CE 17 is refined into CE [53,54,55,56,57,58,59,60] 
* CE 18 is refined into CE [61,62,63,64,65] 


### Cost equations --> "Loop" of fun2/5 
* CEs [60] --> Loop 34 
* CEs [56,58] --> Loop 35 
* CEs [64] --> Loop 36 
* CEs [62,65] --> Loop 37 
* CEs [63] --> Loop 38 
* CEs [54] --> Loop 39 
* CEs [61] --> Loop 40 
* CEs [53,55,57,59] --> Loop 41 
* CEs [52] --> Loop 42 
* CEs [51] --> Loop 43 
* CEs [50] --> Loop 44 

### Ranking functions of CR fun2(V1,V,V7,V6,Out) 
* RF of phase [42,43]: [-V1+V]

#### Partial ranking functions of CR fun2(V1,V,V7,V6,Out) 
* Partial RF of phase [42,43]:
  - RF of loop [42:1,43:1]:
    -V1+V


### Specialization of cost equations length/2 
* CE 36 is refined into CE [66] 
* CE 37 is refined into CE [67] 


### Cost equations --> "Loop" of length/2 
* CEs [67] --> Loop 45 
* CEs [66] --> Loop 46 

### Ranking functions of CR length(V1,Out) 
* RF of phase [45]: [V1]

#### Partial ranking functions of CR length(V1,Out) 
* Partial RF of phase [45]:
  - RF of loop [45:1]:
    V1


### Specialization of cost equations plus/3 
* CE 35 is refined into CE [68] 
* CE 33 is refined into CE [69] 
* CE 34 is refined into CE [70] 


### Cost equations --> "Loop" of plus/3 
* CEs [70] --> Loop 47 
* CEs [68] --> Loop 48 
* CEs [69] --> Loop 49 

### Ranking functions of CR plus(V1,V,Out) 
* RF of phase [47]: [V]

#### Partial ranking functions of CR plus(V1,V,Out) 
* Partial RF of phase [47]:
  - RF of loop [47:1]:
    V


### Specialization of cost equations fun7/3 
* CE 26 is refined into CE [71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112] 
* CE 27 is refined into CE [113,114,115,116,117,118] 
* CE 28 is refined into CE [119] 


### Cost equations --> "Loop" of fun7/3 
* CEs [115,118] --> Loop 50 
* CEs [91,95] --> Loop 51 
* CEs [100,104] --> Loop 52 
* CEs [80,88,111] --> Loop 53 
* CEs [94] --> Loop 54 
* CEs [103] --> Loop 55 
* CEs [79,87,110] --> Loop 56 
* CEs [90] --> Loop 57 
* CEs [74,82,99,106] --> Loop 58 
* CEs [93] --> Loop 59 
* CEs [78,86,102,109] --> Loop 60 
* CEs [92] --> Loop 61 
* CEs [77,85,101,108] --> Loop 62 
* CEs [71,72,73,81,89,96,97,98,105,112] --> Loop 63 
* CEs [113,114,116,117] --> Loop 64 
* CEs [119] --> Loop 65 
* CEs [75,76,83,84,107] --> Loop 66 

### Ranking functions of CR fun7(V1,V,Out) 

#### Partial ranking functions of CR fun7(V1,V,Out) 


### Specialization of cost equations start/5 
* CE 1 is refined into CE [120] 
* CE 2 is refined into CE [121,122] 
* CE 3 is refined into CE [123,124,125,126,127] 
* CE 4 is refined into CE [128,129,130,131,132] 
* CE 5 is refined into CE [133,134] 
* CE 6 is refined into CE [135,136] 
* CE 7 is refined into CE [137,138] 
* CE 8 is refined into CE [139,140,141,142,143,144,145,146,147,148,149,150] 
* CE 9 is refined into CE [151,152] 
* CE 10 is refined into CE [153,154] 
* CE 11 is refined into CE [155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170] 
* CE 12 is refined into CE [171,172,173,174,175] 
* CE 13 is refined into CE [176,177,178,179] 
* CE 14 is refined into CE [180,181] 


### Cost equations --> "Loop" of start/5 
* CEs [133,148] --> Loop 67 
* CEs [130] --> Loop 68 
* CEs [153,172,176] --> Loop 69 
* CEs [121] --> Loop 70 
* CEs [122,123,124,125,126,127] --> Loop 71 
* CEs [120,128,129,131,132,134,135,136,137,138,139,140,141,142,143,144,145,146,147,149,150,151,152,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,173,174,175,177,178,179,180,181] --> Loop 72 

### Ranking functions of CR start(V1,V,V7,V6,V16) 

#### Partial ranking functions of CR start(V1,V,V7,V6,V16) 


Computing Bounds
=====================================

#### Cost of chains of fun(V1,V,Out):
* Chain [[22],23]: 1*it(22)+0
  Such that:it(22) =< Out

  with precondition: [V1>=0,Out>=1,V>=Out] 

* Chain [23]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun1(V1,Out):
* Chain [[24],25]: 1*it(24)+0
  Such that:it(24) =< V1

  with precondition: [Out>=1,V1>=Out] 

* Chain [25]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun6(V1,V,V7,Out):
* Chain [[26],27]: 1*it(26)+0
  Such that:it(26) =< Out

  with precondition: [V=0,Out>=1,V1>=Out,V7>=Out] 

* Chain [27]: 0
  with precondition: [Out=0,V1>=0,V>=0,V7>=0] 


#### Cost of chains of fun4(V1,V,Out):
* Chain [[28],29]: 1*it(28)+0
  Such that:it(28) =< Out

  with precondition: [Out>=1,V1>=Out,V>=Out] 

* Chain [29]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of ge(V1,V,Out):
* Chain [[30],33]: 0
  with precondition: [Out=1,V1>=1,V>=V1+1] 

* Chain [[30],32]: 0
  with precondition: [Out=2,V>=1,V1>=V] 

* Chain [[30],31]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [33]: 0
  with precondition: [V1=0,Out=1,V>=1] 

* Chain [32]: 0
  with precondition: [V=0,Out=2,V1>=0] 

* Chain [31]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun2(V1,V,V7,V6,Out):
* Chain [[42,43],41]: 6*it(42)+1*s(3)+1
  Such that:aux(1) =< V
aux(4) =< -V1+V
it(42) =< aux(4)
s(3) =< it(42)*aux(1)

  with precondition: [V1>=1,V7>=0,V6>=0,Out>=4,V>=V1+1] 

* Chain [[42,43],38]: 6*it(42)+1*s(3)+2*s(4)+3
  Such that:aux(6) =< -V1+V
aux(7) =< V
s(4) =< aux(7)
it(42) =< aux(6)
s(3) =< it(42)*aux(7)

  with precondition: [V7=0,V1>=1,V6>=1,Out>=8,V>=V1+2] 

* Chain [[42,43],37]: 6*it(42)+1*s(3)+1*s(6)+1*s(7)+3
  Such that:s(6) =< V6
aux(8) =< -V1+V
aux(9) =< V
s(7) =< aux(9)
it(42) =< aux(8)
s(3) =< it(42)*aux(9)

  with precondition: [V1>=1,V7>=0,V6>=0,Out>=7,V>=V1+2] 

* Chain [[42,43],36]: 6*it(42)+1*s(3)+3
  Such that:aux(1) =< V
aux(10) =< -V1+V
it(42) =< aux(10)
s(3) =< it(42)*aux(1)

  with precondition: [V1>=1,V7>=0,V6>=0,Out>=6,V>=V1+2] 

* Chain [[42,43],35]: 6*it(42)+1*s(3)+2*s(8)+1
  Such that:aux(11) =< -V1+V
aux(12) =< V
s(8) =< aux(12)
it(42) =< aux(11)
s(3) =< it(42)*aux(12)

  with precondition: [V1>=1,V7>=0,V6>=0,Out>=5,V>=V1+1] 

* Chain [[42,43],34]: 6*it(42)+1*s(3)+1*s(10)+1
  Such that:aux(13) =< -V1+V
aux(14) =< V
s(10) =< aux(14)
it(42) =< aux(13)
s(3) =< it(42)*aux(14)

  with precondition: [V1>=1,V7>=0,V6>=0,V>=V1+1,Out+3*V1>=3*V+2] 

* Chain [44,[42,43],41]: 6*it(42)+1*s(3)+4
  Such that:aux(15) =< V
it(42) =< aux(15)
s(3) =< it(42)*aux(15)

  with precondition: [V1=0,V>=2,V7>=0,V6>=0,Out>=7] 

* Chain [44,[42,43],38]: 8*it(42)+1*s(3)+6
  Such that:aux(16) =< V
it(42) =< aux(16)
s(3) =< it(42)*aux(16)

  with precondition: [V1=0,V7=0,V>=3,V6>=1,Out>=11] 

* Chain [44,[42,43],37]: 7*it(42)+1*s(3)+1*s(6)+6
  Such that:s(6) =< V6
aux(17) =< V
it(42) =< aux(17)
s(3) =< it(42)*aux(17)

  with precondition: [V1=0,V>=3,V7>=0,V6>=0,Out>=10] 

* Chain [44,[42,43],36]: 6*it(42)+1*s(3)+6
  Such that:aux(18) =< V
it(42) =< aux(18)
s(3) =< it(42)*aux(18)

  with precondition: [V1=0,V>=3,V7>=0,V6>=0,Out>=9] 

* Chain [44,[42,43],35]: 8*it(42)+1*s(3)+4
  Such that:aux(19) =< V
it(42) =< aux(19)
s(3) =< it(42)*aux(19)

  with precondition: [V1=0,V>=2,V7>=0,V6>=0,Out>=8] 

* Chain [44,[42,43],34]: 7*it(42)+1*s(3)+4
  Such that:aux(20) =< V
it(42) =< aux(20)
s(3) =< it(42)*aux(20)

  with precondition: [V1=0,V>=2,V7>=0,V6>=0,Out>=3*V+2] 

* Chain [44,41]: 4
  with precondition: [V1=0,Out=4,V>=1,V7>=0,V6>=0] 

* Chain [44,38]: 2*s(4)+6
  Such that:aux(5) =< 1
s(4) =< aux(5)

  with precondition: [V1=0,V7=0,Out=8,V>=2,V6>=1] 

* Chain [44,37]: 1*s(6)+1*s(7)+6
  Such that:s(7) =< 1
s(6) =< V6

  with precondition: [V1=0,Out=7,V>=2,V7>=0,V6>=0] 

* Chain [44,36]: 6
  with precondition: [V1=0,Out=6,V>=2,V7>=0,V6>=0] 

* Chain [44,35]: 1*s(8)+1*s(9)+4
  Such that:s(9) =< 1
s(8) =< V

  with precondition: [V1=0,Out=5,V>=1,V7>=0,V6>=0] 

* Chain [44,34]: 1*s(10)+4
  Such that:s(10) =< 1

  with precondition: [V1=0,V=1,Out=5,V7>=0,V6>=0] 

* Chain [41]: 1
  with precondition: [Out=1,V1>=0,V>=0,V7>=0,V6>=0] 

* Chain [40]: 3
  with precondition: [V1=0,Out=3,V>=1,V7>=0,V6>=0] 

* Chain [39]: 1
  with precondition: [V=0,Out=1,V1>=0,V7>=0,V6>=0] 

* Chain [38]: 2*s(4)+3
  Such that:aux(5) =< V1
s(4) =< aux(5)

  with precondition: [V7=0,V6>=1,Out>=5,V>=V1+1,2*V1+3>=Out,V1+V6+3>=Out] 

* Chain [37]: 1*s(6)+1*s(7)+3
  Such that:s(7) =< V1
s(6) =< V6

  with precondition: [V7>=0,V6>=0,Out>=4,V>=V1+1,V1+3>=Out] 

* Chain [36]: 3
  with precondition: [Out=3,V1>=1,V7>=0,V6>=0,V>=V1+1] 

* Chain [35]: 1*s(8)+1*s(9)+1
  Such that:s(9) =< V1
s(8) =< V

  with precondition: [V7>=0,V6>=0,Out>=2,V1+1>=Out,V+1>=Out] 

* Chain [34]: 1*s(10)+1
  Such that:s(10) =< V

  with precondition: [V7>=0,V6>=0,Out>=2,V1>=V,V+1>=Out] 


#### Cost of chains of length(V1,Out):
* Chain [[45],46]: 0
  with precondition: [Out>=1,V1>=Out] 

* Chain [46]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of plus(V1,V,Out):
* Chain [[47],49]: 0
  with precondition: [V+V1=Out,V1>=0,V>=1] 

* Chain [[47],48]: 0
  with precondition: [V1>=0,Out>=1,V>=Out] 

* Chain [49]: 0
  with precondition: [V=0,V1=Out,V1>=0] 

* Chain [48]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun7(V1,V,Out):
* Chain [66]: 121*s(67)+6*s(69)+17*s(71)+6
  Such that:aux(30) =< 1
aux(31) =< V
s(67) =< aux(31)
s(69) =< aux(30)
s(71) =< s(67)*aux(31)

  with precondition: [V1>=0,V>=2,Out>=8] 

* Chain [65]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [64]: 0
  with precondition: [Out=1,V1>=0,V>=0] 

* Chain [63]: 1
  with precondition: [Out=2,V1>=0,V>=0] 

* Chain [62]: 3
  with precondition: [Out=4,V1>=0,V>=1] 

* Chain [61]: 3
  with precondition: [Out=4,V1>=1,V>=0] 

* Chain [60]: 4
  with precondition: [Out=5,V1>=0,V>=1] 

* Chain [59]: 4
  with precondition: [Out=5,V1>=1,V>=0] 

* Chain [58]: 3*s(90)+8*s(92)+1*s(96)+4
  Such that:s(96) =< V1+V
aux(32) =< 1
aux(33) =< V
s(90) =< aux(33)
s(92) =< aux(32)

  with precondition: [Out=6,V1>=0,V>=1] 

* Chain [57]: 1*s(102)+2*s(104)+4
  Such that:s(103) =< 1
s(102) =< V1
s(104) =< s(103)

  with precondition: [Out=6,V1>=1,V>=0] 

* Chain [56]: 6
  with precondition: [Out=7,V1>=0,V>=2] 

* Chain [55]: 6
  with precondition: [Out=7,V1>=1,V>=1] 

* Chain [54]: 6
  with precondition: [Out=7,V1>=2,V>=0] 

* Chain [53]: 3*s(105)+3*s(106)+6
  Such that:aux(34) =< 1
aux(35) =< V
s(105) =< aux(34)
s(106) =< aux(35)

  with precondition: [Out=8,V1>=0,V>=2] 

* Chain [52]: 2*s(112)+3*s(114)+34*s(115)+5*s(116)+6
  Such that:s(113) =< V1+V
aux(36) =< 1
aux(37) =< V
s(114) =< aux(36)
s(112) =< aux(37)
s(115) =< s(113)
s(116) =< s(115)*s(113)

  with precondition: [V1>=1,V>=1,Out>=8] 

* Chain [51]: 2*s(120)+3*s(122)+34*s(123)+5*s(124)+6
  Such that:s(121) =< V1
aux(38) =< 1
aux(39) =< V
s(122) =< aux(38)
s(120) =< aux(39)
s(123) =< s(121)
s(124) =< s(123)*s(121)

  with precondition: [V1>=2,V>=0,Out>=8] 

* Chain [50]: 2*s(127)+0
  Such that:aux(40) =< V
s(127) =< aux(40)

  with precondition: [V1>=0,Out>=2,V+1>=Out] 


#### Cost of chains of start(V1,V,V7,V6,V16):
* Chain [72]: 2*s(138)+6*s(142)+194*s(143)+72*s(144)+12*s(145)+38*s(150)+30*s(153)+23*s(159)+35*s(177)+5*s(198)+5*s(205)+6
  Such that:aux(43) =< 1
aux(44) =< -V1+V
aux(45) =< V1
aux(46) =< V1+1
aux(47) =< V1+V
aux(48) =< V
aux(49) =< V6
s(153) =< aux(43)
s(150) =< aux(45)
s(138) =< aux(46)
s(177) =< aux(47)
s(143) =< aux(48)
s(142) =< aux(49)
s(159) =< s(143)*aux(48)
s(198) =< s(177)*aux(47)
s(205) =< s(150)*aux(45)
s(144) =< aux(44)
s(145) =< s(144)*aux(48)

  with precondition: [V1>=0] 

* Chain [71]: 4*s(206)+2*s(210)+8*s(211)+36*s(212)+6*s(213)+5
  Such that:s(207) =< -V+V7
s(209) =< V16
aux(50) =< V+1
aux(51) =< V7
s(206) =< aux(50)
s(210) =< s(209)
s(211) =< aux(51)
s(212) =< s(207)
s(213) =< s(212)*aux(51)

  with precondition: [V1=1,V>=0,V7>=0,V6>=0,V16>=0] 

* Chain [70]: 1*s(219)+2
  Such that:s(219) =< V16

  with precondition: [V1=1,V6=0,V>=1,V7>=0,V16>=1] 

* Chain [69]: 1*s(220)+0
  Such that:s(220) =< V7

  with precondition: [V=0,V1>=0] 

* Chain [68]: 2*s(222)+4
  Such that:s(221) =< V1+1
s(222) =< s(221)

  with precondition: [V7=0,V1>=0,V6>=1,V>=V1+2] 

* Chain [67]: 1*s(223)+2*s(225)+3
  Such that:s(224) =< V1
s(223) =< V6
s(225) =< s(224)

  with precondition: [V7=0,V1>=1,V>=0,V6>=1] 


Closed-form bounds of start(V1,V,V7,V6,V16): 
-------------------------------------
* Chain [72] with precondition: [V1>=0] 
    - Upper bound: 38*V1+36+5*V1*V1+nat(V)*194+nat(V)*23*nat(V)+nat(V)*12*nat(-V1+V)+nat(V6)*6+nat(V1+V)*35+nat(V1+V)*5*nat(V1+V)+(2*V1+2)+nat(-V1+V)*72 
    - Complexity: n^2 
* Chain [71] with precondition: [V1=1,V>=0,V7>=0,V6>=0,V16>=0] 
    - Upper bound: 8*V7+5+6*V7*nat(-V+V7)+2*V16+(4*V+4)+nat(-V+V7)*36 
    - Complexity: n^2 
* Chain [70] with precondition: [V1=1,V6=0,V>=1,V7>=0,V16>=1] 
    - Upper bound: V16+2 
    - Complexity: n 
* Chain [69] with precondition: [V=0,V1>=0] 
    - Upper bound: nat(V7) 
    - Complexity: n 
* Chain [68] with precondition: [V7=0,V1>=0,V6>=1,V>=V1+2] 
    - Upper bound: 2*V1+6 
    - Complexity: n 
* Chain [67] with precondition: [V7=0,V1>=1,V>=0,V6>=1] 
    - Upper bound: 2*V1+V6+3 
    - Complexity: n 

### Maximum cost of start(V1,V,V7,V6,V16): max([max([max([2*V1+4,nat(V16)])+2,nat(V7)*7+5+nat(V7)*6*nat(-V+V7)+nat(V16)*2+nat(V+1)*4+nat(-V+V7)*36+nat(V7)]),36*V1+33+5*V1*V1+nat(V)*194+nat(V)*23*nat(V)+nat(V)*12*nat(-V1+V)+nat(V6)*5+nat(V1+V)*35+nat(V1+V)*5*nat(V1+V)+(2*V1+2)+nat(-V1+V)*72+(2*V1+3+nat(V6))]) 
Asymptotic class: n^2 
* Total analysis performed in 1214 ms.


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

(24)
BOUNDS(1, n^2)

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

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

(26)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))
Tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0) -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0) -> c7
   GE(0, s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0, cons(z0, xs), z1) -> c12
   TAKE(0, nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
S tuples:
   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0) -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0) -> c7
   GE(0, s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0, cons(z0, xs), z1) -> c12
   TAKE(0, nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
K tuples:none
Defined Rule Symbols:   app_2, plus_2, length_1, helpa_4, ge_2, if_5, take_3, helpb_4

Defined Pair Symbols:   APP_2, PLUS_2, LENGTH_1, HELPA_4, GE_2, IF_5, TAKE_3, HELPB_4

Compound Symbols:   c_3, c1_3, c2, c3_1, c4, c5_1, c6_2, c7, c8, c9_1, c10, c11_1, c12, c13, c14_1, c15_1, c16_1, c17_1


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

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

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

   APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0) -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0) -> c7
   GE(0, s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0, cons(z0, xs), z1) -> c12
   TAKE(0, nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))

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

   app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0, cons(z0, xs), z1) -> z0
   take(0, nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

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

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

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

   APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
   APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
   PLUS(z0, 0') -> c2
   PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
   LENGTH(nil) -> c4
   LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
   HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   GE(z0, 0') -> c7
   GE(0', s(z0)) -> c8
   GE(s(z0), s(z1)) -> c9(GE(z0, z1))
   IF(true, z0, z1, z2, z3) -> c10
   IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
   TAKE(0', cons(z0, xs), z1) -> c12
   TAKE(0', nil, cons(z0, z1)) -> c13
   TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
   TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
   HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
   HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))

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

   app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
   plus(z0, 0') -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   length(nil) -> 0'
   length(cons(z0, z1)) -> s(length(z1))
   helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   if(true, z0, z1, z2, z3) -> nil
   if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
   take(0', cons(z0, xs), z1) -> z0
   take(0', nil, cons(z0, z1)) -> z0
   take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
   take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
   helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

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

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

(32)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15

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

(33) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
HELPA, plus, length, PLUS, LENGTH, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(34)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
plus, HELPA, length, PLUS, LENGTH, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)

Induction Base:
plus(gen_0':s16_18(a), gen_0':s16_18(0)) ->_R^Omega(0)
gen_0':s16_18(a)

Induction Step:
plus(gen_0':s16_18(a), gen_0':s16_18(+(n20_18, 1))) ->_R^Omega(0)
s(plus(gen_0':s16_18(a), gen_0':s16_18(n20_18))) ->_IH
s(gen_0':s16_18(+(a, c21_18)))

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

(36)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
length, HELPA, PLUS, LENGTH, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)

Induction Base:
length(gen_nil:cons:xs13_18(0)) ->_R^Omega(0)
0'

Induction Step:
length(gen_nil:cons:xs13_18(+(n1801_18, 1))) ->_R^Omega(0)
s(length(gen_nil:cons:xs13_18(n1801_18))) ->_IH
s(gen_0':s16_18(c1802_18))

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:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
PLUS, HELPA, LENGTH, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)

Induction Base:
PLUS(gen_0':s16_18(a), gen_0':s16_18(0)) ->_R^Omega(1)
c2

Induction Step:
PLUS(gen_0':s16_18(a), gen_0':s16_18(+(n2266_18, 1))) ->_R^Omega(1)
c3(PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18))) ->_IH
c3(gen_c2:c314_18(c2267_18))

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

(40)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
PLUS, HELPA, LENGTH, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

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

(43)
BOUNDS(n^1, INF)

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

(44)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
LENGTH, HELPA, ge, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(45) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)

Induction Base:
LENGTH(gen_nil:cons:xs13_18(0)) ->_R^Omega(1)
c4

Induction Step:
LENGTH(gen_nil:cons:xs13_18(+(n3061_18, 1))) ->_R^Omega(1)
c5(LENGTH(gen_nil:cons:xs13_18(n3061_18))) ->_IH
c5(gen_c4:c515_18(c3062_18))

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

(46)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
ge, HELPA, GE, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
ge < HELPA
GE < HELPA
HELPA = HELPB
ge < helpa
TAKE < HELPB
helpa = helpb
take < helpb

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

(47) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s16_18(0), gen_0':s16_18(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s16_18(+(n3498_18, 1)), gen_0':s16_18(+(n3498_18, 1))) ->_R^Omega(0)
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) ->_IH
true

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

(48)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
GE, HELPA, HELPB, TAKE, helpa, helpb, take

They will be analysed ascendingly in the following order:
GE < HELPA
HELPA = HELPB
TAKE < HELPB
helpa = helpb
take < helpb

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

(49) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s16_18(n3956_18), gen_0':s16_18(n3956_18)) -> gen_c7:c8:c917_18(n3956_18), rt in Omega(1 + n3956_18)

Induction Base:
GE(gen_0':s16_18(0), gen_0':s16_18(0)) ->_R^Omega(1)
c7

Induction Step:
GE(gen_0':s16_18(+(n3956_18, 1)), gen_0':s16_18(+(n3956_18, 1))) ->_R^Omega(1)
c9(GE(gen_0':s16_18(n3956_18), gen_0':s16_18(n3956_18))) ->_IH
c9(gen_c7:c8:c917_18(c3957_18))

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

(50)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) -> true, rt in Omega(0)
GE(gen_0':s16_18(n3956_18), gen_0':s16_18(n3956_18)) -> gen_c7:c8:c917_18(n3956_18), rt in Omega(1 + n3956_18)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
TAKE, HELPA, HELPB, helpa, helpb, take

They will be analysed ascendingly in the following order:
HELPA = HELPB
TAKE < HELPB
helpa = helpb
take < helpb

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

(51) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TAKE(gen_0':s16_18(+(1, n4814_18)), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, n4814_18))) -> *19_18, rt in Omega(n4814_18)

Induction Base:
TAKE(gen_0':s16_18(+(1, 0)), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, 0)))

Induction Step:
TAKE(gen_0':s16_18(+(1, +(n4814_18, 1))), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, +(n4814_18, 1)))) ->_R^Omega(1)
c15(TAKE(gen_0':s16_18(+(1, n4814_18)), nil, gen_nil:cons:xs13_18(+(1, n4814_18)))) ->_IH
c15(*19_18)

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

(52)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) -> true, rt in Omega(0)
GE(gen_0':s16_18(n3956_18), gen_0':s16_18(n3956_18)) -> gen_c7:c8:c917_18(n3956_18), rt in Omega(1 + n3956_18)
TAKE(gen_0':s16_18(+(1, n4814_18)), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, n4814_18))) -> *19_18, rt in Omega(n4814_18)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
take, HELPA, HELPB, helpa, helpb

They will be analysed ascendingly in the following order:
HELPA = HELPB
helpa = helpb
take < helpb

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

(53) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
take(gen_0':s16_18(n8519_18), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, n8519_18))) -> hole_take7_18, rt in Omega(0)

Induction Base:
take(gen_0':s16_18(0), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, 0))) ->_R^Omega(0)
hole_take7_18

Induction Step:
take(gen_0':s16_18(+(n8519_18, 1)), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, +(n8519_18, 1)))) ->_R^Omega(0)
take(gen_0':s16_18(n8519_18), nil, gen_nil:cons:xs13_18(+(1, n8519_18))) ->_IH
hole_take7_18

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

(54)
Obligation:
Innermost TRS:
Rules:
APP(z0, z1) -> c(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0))
APP(z0, z1) -> c1(HELPA(0', plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1))
PLUS(z0, 0') -> c2
PLUS(z0, s(z1)) -> c3(PLUS(z0, z1))
LENGTH(nil) -> c4
LENGTH(cons(z0, z1)) -> c5(LENGTH(z1))
HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
GE(z0, 0') -> c7
GE(0', s(z0)) -> c8
GE(s(z0), s(z1)) -> c9(GE(z0, z1))
IF(true, z0, z1, z2, z3) -> c10
IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3))
TAKE(0', cons(z0, xs), z1) -> c12
TAKE(0', nil, cons(z0, z1)) -> c13
TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2))
TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2))
HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3))
HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3))
app(z0, z1) -> helpa(0', plus(length(z0), length(z1)), z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3)
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
if(true, z0, z1, z2, z3) -> nil
if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3)
take(0', cons(z0, xs), z1) -> z0
take(0', nil, cons(z0, z1)) -> z0
take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2)
take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2)
helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3))

Types:
APP :: nil:cons:xs -> nil:cons:xs -> c:c1
c :: c6 -> c2:c3 -> c4:c5 -> c:c1
HELPA :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c6
0' :: 0':s
plus :: 0':s -> 0':s -> 0':s
length :: nil:cons:xs -> 0':s
PLUS :: 0':s -> 0':s -> c2:c3
LENGTH :: nil:cons:xs -> c4:c5
c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3 -> c2:c3
nil :: nil:cons:xs
c4 :: c4:c5
cons :: take -> nil:cons:xs -> nil:cons:xs
c5 :: c4:c5 -> c4:c5
c6 :: c10:c11 -> c7:c8:c9 -> c6
IF :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c10:c11
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c16:c17 -> c10:c11
HELPB :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> c16:c17
TAKE :: 0':s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15
xs :: nil:cons:xs
c12 :: c12:c13:c14:c15
c13 :: c12:c13:c14:c15
c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15
c16 :: c12:c13:c14:c15 -> c16:c17
c17 :: c6 -> c16:c17
app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpa :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
if :: true:false -> 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
helpb :: 0':s -> 0':s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs
take :: 0':s -> nil:cons:xs -> nil:cons:xs -> take
hole_c:c11_18 :: c:c1
hole_nil:cons:xs2_18 :: nil:cons:xs
hole_c63_18 :: c6
hole_c2:c34_18 :: c2:c3
hole_c4:c55_18 :: c4:c5
hole_0':s6_18 :: 0':s
hole_take7_18 :: take
hole_c10:c118_18 :: c10:c11
hole_c7:c8:c99_18 :: c7:c8:c9
hole_true:false10_18 :: true:false
hole_c16:c1711_18 :: c16:c17
hole_c12:c13:c14:c1512_18 :: c12:c13:c14:c15
gen_nil:cons:xs13_18 :: Nat -> nil:cons:xs
gen_c2:c314_18 :: Nat -> c2:c3
gen_c4:c515_18 :: Nat -> c4:c5
gen_0':s16_18 :: Nat -> 0':s
gen_c7:c8:c917_18 :: Nat -> c7:c8:c9
gen_c12:c13:c14:c1518_18 :: Nat -> c12:c13:c14:c15


Lemmas:
plus(gen_0':s16_18(a), gen_0':s16_18(n20_18)) -> gen_0':s16_18(+(n20_18, a)), rt in Omega(0)
length(gen_nil:cons:xs13_18(n1801_18)) -> gen_0':s16_18(n1801_18), rt in Omega(0)
PLUS(gen_0':s16_18(a), gen_0':s16_18(n2266_18)) -> gen_c2:c314_18(n2266_18), rt in Omega(1 + n2266_18)
LENGTH(gen_nil:cons:xs13_18(n3061_18)) -> gen_c4:c515_18(n3061_18), rt in Omega(1 + n3061_18)
ge(gen_0':s16_18(n3498_18), gen_0':s16_18(n3498_18)) -> true, rt in Omega(0)
GE(gen_0':s16_18(n3956_18), gen_0':s16_18(n3956_18)) -> gen_c7:c8:c917_18(n3956_18), rt in Omega(1 + n3956_18)
TAKE(gen_0':s16_18(+(1, n4814_18)), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, n4814_18))) -> *19_18, rt in Omega(n4814_18)
take(gen_0':s16_18(n8519_18), gen_nil:cons:xs13_18(0), gen_nil:cons:xs13_18(+(1, n8519_18))) -> hole_take7_18, rt in Omega(0)


Generator Equations:
gen_nil:cons:xs13_18(0) <=> nil
gen_nil:cons:xs13_18(+(x, 1)) <=> cons(hole_take7_18, gen_nil:cons:xs13_18(x))
gen_c2:c314_18(0) <=> c2
gen_c2:c314_18(+(x, 1)) <=> c3(gen_c2:c314_18(x))
gen_c4:c515_18(0) <=> c4
gen_c4:c515_18(+(x, 1)) <=> c5(gen_c4:c515_18(x))
gen_0':s16_18(0) <=> 0'
gen_0':s16_18(+(x, 1)) <=> s(gen_0':s16_18(x))
gen_c7:c8:c917_18(0) <=> c7
gen_c7:c8:c917_18(+(x, 1)) <=> c9(gen_c7:c8:c917_18(x))
gen_c12:c13:c14:c1518_18(0) <=> c12
gen_c12:c13:c14:c1518_18(+(x, 1)) <=> c14(gen_c12:c13:c14:c1518_18(x))


The following defined symbols remain to be analysed:
helpb, HELPA, HELPB, helpa

They will be analysed ascendingly in the following order:
HELPA = HELPB
helpa = helpb