WORST_CASE(Omega(n^1),?)
proof of input_CTMhGGahM1.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, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 61 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 33 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 2518 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 83 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 77 ms]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs


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

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


The TRS R consists of the following rules:

   divide_ys#1(x2, x1) -> Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
   cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) -> Cons(x4, merge#2(x3, Cons(x5, x6)))
   cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) -> Cons(x2, merge#2(Cons(x7, x8), x1))
   merge#2(Nil, x2) -> x2
   merge#2(Cons(x4, x2), Nil) -> Cons(x4, x2)
   merge#2(Cons(x8, x6), Cons(x4, x2)) -> cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) -> Cons(x229, Nil)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) -> const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
   drop#2(0, x2) -> x2
   drop#2(S(0), Nil) -> bot[1]
   drop#2(S(x10), Cons(x56, x64)) -> drop#2(x10, x64)
   take#2(0, x2) -> Nil
   take#2(S(0), Nil) -> Cons(bot[0], Nil)
   take#2(S(x22), Cons(x56, x64)) -> Cons(x56, take#2(x22, x64))
   halve#1(0) -> 0
   halve#1(S(0)) -> S(0)
   halve#1(S(S(x14))) -> S(halve#1(x14))
   const_f#2(x3, Cons(x6, Cons(x4, x2))) -> merge#2(x6, x4)
   leq#2(0, x16) -> True
   leq#2(S(x20), 0) -> False
   leq#2(S(x4), S(x2)) -> leq#2(x4, x2)
   length#1(Nil) -> 0
   length#1(Cons(x6, x8)) -> S(length#1(x8))
   map#2(dc(x2, x4, x6, x8, x10), Nil) -> Nil
   map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) -> Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
   main(x113) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
   cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
   cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
   merge#2(Nil, z0) -> z0
   merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
   drop#2(0, z0) -> z0
   drop#2(S(0), Nil) -> bot[1]
   drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
   take#2(0, z0) -> Nil
   take#2(S(0), Nil) -> Cons(bot[0], Nil)
   take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
   halve#1(0) -> 0
   halve#1(S(0)) -> S(0)
   halve#1(S(S(z0))) -> S(halve#1(z0))
   const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
   leq#2(0, z0) -> True
   leq#2(S(z0), 0) -> False
   leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
   length#1(Nil) -> 0
   length#1(Cons(z0, z1)) -> S(length#1(z1))
   map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
   map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
   main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)
Tuples:
   DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
   DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
   COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
   COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
   MERGE#2(Nil, z0) -> c4
   MERGE#2(Cons(z0, z1), Nil) -> c5
   MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
   DROP#2(0, z0) -> c10
   DROP#2(S(0), Nil) -> c11
   DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
   TAKE#2(0, z0) -> c13
   TAKE#2(S(0), Nil) -> c14
   TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
   HALVE#1(0) -> c16
   HALVE#1(S(0)) -> c17
   HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
   CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
   LEQ#2(0, z0) -> c20
   LEQ#2(S(z0), 0) -> c21
   LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
   LENGTH#1(Nil) -> c23
   LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
   MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
   MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
S tuples:
   DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
   DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
   COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
   COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
   MERGE#2(Nil, z0) -> c4
   MERGE#2(Cons(z0, z1), Nil) -> c5
   MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
   DROP#2(0, z0) -> c10
   DROP#2(S(0), Nil) -> c11
   DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
   TAKE#2(0, z0) -> c13
   TAKE#2(S(0), Nil) -> c14
   TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
   HALVE#1(0) -> c16
   HALVE#1(S(0)) -> c17
   HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
   CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
   LEQ#2(0, z0) -> c20
   LEQ#2(S(z0), 0) -> c21
   LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
   LENGTH#1(Nil) -> c23
   LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
   MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
   MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
K tuples:none
Defined Rule Symbols:   divide_ys#1_2, cond_merge_ys_zs_2_7, merge#2_2, dc#1_6, drop#2_2, take#2_2, halve#1_1, const_f#2_2, leq#2_2, length#1_1, map#2_2, main_1

Defined Pair Symbols:   DIVIDE_YS#1_2, COND_MERGE_YS_ZS_2_7, MERGE#2_2, DC#1_6, DROP#2_2, TAKE#2_2, HALVE#1_1, CONST_F#2_2, LEQ#2_2, LENGTH#1_1, MAP#2_2, MAIN_1

Compound Symbols:   c_1, c1_1, c2_1, c3_1, c4, c5, c6_2, c7, c8, c9_5, c10, c11, c12_1, c13, c14, c15_1, c16, c17, c18_1, c19_1, c20, c21, c22_1, c23, c24_1, c25, c26_1, c27_1, c28_1


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

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

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

   DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
   DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
   COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
   COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
   MERGE#2(Nil, z0) -> c4
   MERGE#2(Cons(z0, z1), Nil) -> c5
   MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
   DROP#2(0, z0) -> c10
   DROP#2(S(0), Nil) -> c11
   DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
   TAKE#2(0, z0) -> c13
   TAKE#2(S(0), Nil) -> c14
   TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
   HALVE#1(0) -> c16
   HALVE#1(S(0)) -> c17
   HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
   CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
   LEQ#2(0, z0) -> c20
   LEQ#2(S(z0), 0) -> c21
   LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
   LENGTH#1(Nil) -> c23
   LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
   MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
   MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))

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

   divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
   cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
   cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
   merge#2(Nil, z0) -> z0
   merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
   drop#2(0, z0) -> z0
   drop#2(S(0), Nil) -> bot[1]
   drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
   take#2(0, z0) -> Nil
   take#2(S(0), Nil) -> Cons(bot[0], Nil)
   take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
   halve#1(0) -> 0
   halve#1(S(0)) -> S(0)
   halve#1(S(S(z0))) -> S(halve#1(z0))
   const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
   leq#2(0, z0) -> True
   leq#2(S(z0), 0) -> False
   leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
   length#1(Nil) -> 0
   length#1(Cons(z0, z1)) -> S(length#1(z1))
   map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
   map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
   main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

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

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

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

   DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
   DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
   COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
   COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
   MERGE#2(Nil, z0) -> c4
   MERGE#2(Cons(z0, z1), Nil) -> c5
   MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
   DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
   DROP#2(0', z0) -> c10
   DROP#2(S(0'), Nil) -> c11
   DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
   TAKE#2(0', z0) -> c13
   TAKE#2(S(0'), Nil) -> c14
   TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
   HALVE#1(0') -> c16
   HALVE#1(S(0')) -> c17
   HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
   CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
   LEQ#2(0', z0) -> c20
   LEQ#2(S(z0), 0') -> c21
   LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
   LENGTH#1(Nil) -> c23
   LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
   MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
   MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
   MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))

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

   divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
   cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
   cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
   merge#2(Nil, z0) -> z0
   merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
   dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
   drop#2(0', z0) -> z0
   drop#2(S(0'), Nil) -> bot[1]
   drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
   take#2(0', z0) -> Nil
   take#2(S(0'), Nil) -> Cons(bot[0], Nil)
   take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
   halve#1(0') -> 0'
   halve#1(S(0')) -> S(0')
   halve#1(S(S(z0))) -> S(halve#1(z0))
   const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
   leq#2(0', z0) -> True
   leq#2(S(z0), 0') -> False
   leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
   length#1(Nil) -> 0'
   length#1(Cons(z0, z1)) -> S(length#1(z1))
   map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
   map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
   main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
TAKE#2, DROP#2, MERGE#2, leq#2, LEQ#2, map#2, halve#1, length#1, MAP#2, HALVE#1, LENGTH#1, take#2, drop#2, merge#2

They will be analysed ascendingly in the following order:
leq#2 < MERGE#2
LEQ#2 < MERGE#2
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2
map#2 < MAP#2
halve#1 < MAP#2
length#1 < MAP#2
HALVE#1 < MAP#2
LENGTH#1 < MAP#2

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

(10)
Obligation:
Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24


Generator Equations:
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0) <=> Nil
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(x))
gen_c13:c14:c1522_29(0) <=> c13
gen_c13:c14:c1522_29(+(x, 1)) <=> c15(gen_c13:c14:c1522_29(x))
gen_c10:c11:c1223_29(0) <=> c10
gen_c10:c11:c1223_29(+(x, 1)) <=> c12(gen_c10:c11:c1223_29(x))
gen_c20:c21:c2224_29(0) <=> c20
gen_c20:c21:c2224_29(+(x, 1)) <=> c22(gen_c20:c21:c2224_29(x))
gen_c25:c26:c2725_29(0) <=> c25
gen_c25:c26:c2725_29(+(x, 1)) <=> c27(gen_c25:c26:c2725_29(x))
gen_c16:c17:c1826_29(0) <=> c16
gen_c16:c17:c1826_29(+(x, 1)) <=> c18(gen_c16:c17:c1826_29(x))
gen_c23:c2427_29(0) <=> c23
gen_c23:c2427_29(+(x, 1)) <=> c24(gen_c23:c2427_29(x))


The following defined symbols remain to be analysed:
TAKE#2, DROP#2, MERGE#2, leq#2, LEQ#2, map#2, halve#1, length#1, MAP#2, HALVE#1, LENGTH#1, take#2, drop#2, merge#2

They will be analysed ascendingly in the following order:
leq#2 < MERGE#2
LEQ#2 < MERGE#2
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2
map#2 < MAP#2
halve#1 < MAP#2
length#1 < MAP#2
HALVE#1 < MAP#2
LENGTH#1 < MAP#2

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29))) -> *28_29, rt in Omega(0)

Induction Base:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, 0)))

Induction Step:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, +(n5083_29, 1)))) ->_R^Omega(0)
S(length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29)))) ->_IH
S(*28_29)

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

(12)
Obligation:
Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24


Lemmas:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29))) -> *28_29, rt in Omega(0)


Generator Equations:
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0) <=> Nil
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(x))
gen_c13:c14:c1522_29(0) <=> c13
gen_c13:c14:c1522_29(+(x, 1)) <=> c15(gen_c13:c14:c1522_29(x))
gen_c10:c11:c1223_29(0) <=> c10
gen_c10:c11:c1223_29(+(x, 1)) <=> c12(gen_c10:c11:c1223_29(x))
gen_c20:c21:c2224_29(0) <=> c20
gen_c20:c21:c2224_29(+(x, 1)) <=> c22(gen_c20:c21:c2224_29(x))
gen_c25:c26:c2725_29(0) <=> c25
gen_c25:c26:c2725_29(+(x, 1)) <=> c27(gen_c25:c26:c2725_29(x))
gen_c16:c17:c1826_29(0) <=> c16
gen_c16:c17:c1826_29(+(x, 1)) <=> c18(gen_c16:c17:c1826_29(x))
gen_c23:c2427_29(0) <=> c23
gen_c23:c2427_29(+(x, 1)) <=> c24(gen_c23:c2427_29(x))


The following defined symbols remain to be analysed:
map#2, MAP#2, HALVE#1, LENGTH#1, take#2, drop#2, merge#2

They will be analysed ascendingly in the following order:
map#2 < MAP#2
HALVE#1 < MAP#2
LENGTH#1 < MAP#2

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29)) -> gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29), rt in Omega(0)

Induction Base:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0)) ->_R^Omega(0)
Nil

Induction Step:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(n5700_29, 1))) ->_R^Omega(0)
Cons(dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29))) ->_R^Omega(0)
Cons(Nil, map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29))) ->_IH
Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(c5701_29))

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

(14)
Obligation:
Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24


Lemmas:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29))) -> *28_29, rt in Omega(0)
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29)) -> gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0) <=> Nil
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(x))
gen_c13:c14:c1522_29(0) <=> c13
gen_c13:c14:c1522_29(+(x, 1)) <=> c15(gen_c13:c14:c1522_29(x))
gen_c10:c11:c1223_29(0) <=> c10
gen_c10:c11:c1223_29(+(x, 1)) <=> c12(gen_c10:c11:c1223_29(x))
gen_c20:c21:c2224_29(0) <=> c20
gen_c20:c21:c2224_29(+(x, 1)) <=> c22(gen_c20:c21:c2224_29(x))
gen_c25:c26:c2725_29(0) <=> c25
gen_c25:c26:c2725_29(+(x, 1)) <=> c27(gen_c25:c26:c2725_29(x))
gen_c16:c17:c1826_29(0) <=> c16
gen_c16:c17:c1826_29(+(x, 1)) <=> c18(gen_c16:c17:c1826_29(x))
gen_c23:c2427_29(0) <=> c23
gen_c23:c2427_29(+(x, 1)) <=> c24(gen_c23:c2427_29(x))


The following defined symbols remain to be analysed:
HALVE#1, MAP#2, LENGTH#1, take#2, drop#2, merge#2

They will be analysed ascendingly in the following order:
HALVE#1 < MAP#2
LENGTH#1 < MAP#2

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n6404_29)) -> gen_c23:c2427_29(n6404_29), rt in Omega(1 + n6404_29)

Induction Base:
LENGTH#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0)) ->_R^Omega(1)
c23

Induction Step:
LENGTH#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(n6404_29, 1))) ->_R^Omega(1)
c24(LENGTH#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n6404_29))) ->_IH
c24(gen_c23:c2427_29(c6405_29))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24


Lemmas:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29))) -> *28_29, rt in Omega(0)
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29)) -> gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0) <=> Nil
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(x))
gen_c13:c14:c1522_29(0) <=> c13
gen_c13:c14:c1522_29(+(x, 1)) <=> c15(gen_c13:c14:c1522_29(x))
gen_c10:c11:c1223_29(0) <=> c10
gen_c10:c11:c1223_29(+(x, 1)) <=> c12(gen_c10:c11:c1223_29(x))
gen_c20:c21:c2224_29(0) <=> c20
gen_c20:c21:c2224_29(+(x, 1)) <=> c22(gen_c20:c21:c2224_29(x))
gen_c25:c26:c2725_29(0) <=> c25
gen_c25:c26:c2725_29(+(x, 1)) <=> c27(gen_c25:c26:c2725_29(x))
gen_c16:c17:c1826_29(0) <=> c16
gen_c16:c17:c1826_29(+(x, 1)) <=> c18(gen_c16:c17:c1826_29(x))
gen_c23:c2427_29(0) <=> c23
gen_c23:c2427_29(+(x, 1)) <=> c24(gen_c23:c2427_29(x))


The following defined symbols remain to be analysed:
LENGTH#1, MAP#2, take#2, drop#2, merge#2

They will be analysed ascendingly in the following order:
LENGTH#1 < MAP#2

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
DIVIDE_YS#1(z0, z1) -> c(TAKE#2(z1, z0))
DIVIDE_YS#1(z0, z1) -> c1(DROP#2(z1, z0))
COND_MERGE_YS_ZS_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c2(MERGE#2(z5, Cons(z2, z3)))
COND_MERGE_YS_ZS_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> c3(MERGE#2(Cons(z0, z1), z7))
MERGE#2(Nil, z0) -> c4
MERGE#2(Cons(z0, z1), Nil) -> c5
MERGE#2(Cons(z0, z1), Cons(z2, z3)) -> c6(COND_MERGE_YS_ZS_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3), LEQ#2(z0, z2))
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> c7
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> c8
DC#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> c9(CONST_F#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))))), MAP#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))), DIVIDE_YS#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2)))), HALVE#1(length#1(z2)), LENGTH#1(z2))
DROP#2(0', z0) -> c10
DROP#2(S(0'), Nil) -> c11
DROP#2(S(z0), Cons(z1, z2)) -> c12(DROP#2(z0, z2))
TAKE#2(0', z0) -> c13
TAKE#2(S(0'), Nil) -> c14
TAKE#2(S(z0), Cons(z1, z2)) -> c15(TAKE#2(z0, z2))
HALVE#1(0') -> c16
HALVE#1(S(0')) -> c17
HALVE#1(S(S(z0))) -> c18(HALVE#1(z0))
CONST_F#2(z0, Cons(z1, Cons(z2, z3))) -> c19(MERGE#2(z1, z2))
LEQ#2(0', z0) -> c20
LEQ#2(S(z0), 0') -> c21
LEQ#2(S(z0), S(z1)) -> c22(LEQ#2(z0, z1))
LENGTH#1(Nil) -> c23
LENGTH#1(Cons(z0, z1)) -> c24(LENGTH#1(z1))
MAP#2(dc(z0, z1, z2, z3, z4), Nil) -> c25
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c26(DC#1(z0, z1, z2, z3, z4, z5))
MAP#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> c27(MAP#2(dc(z0, z1, z2, z3, z4), z6))
MAIN(z0) -> c28(DC#1(map, divisible, mergesort_zs_3, divide, const_f, z0))
divide_ys#1(z0, z1) -> Cons(take#2(z1, z0), Cons(drop#2(z1, z0), Nil))
cond_merge_ys_zs_2(True, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z4, merge#2(z5, Cons(z2, z3)))
cond_merge_ys_zs_2(False, Cons(z0, z1), Cons(z2, z3), z4, z5, z6, z7) -> Cons(z6, merge#2(Cons(z0, z1), z7))
merge#2(Nil, z0) -> z0
merge#2(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge#2(Cons(z0, z1), Cons(z2, z3)) -> cond_merge_ys_zs_2(leq#2(z0, z2), Cons(z0, z1), Cons(z2, z3), z0, z1, z2, z3)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) -> Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Nil)) -> Cons(z0, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(z0, Cons(z1, z2))) -> const_f#2(Cons(z0, Cons(z1, z2)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(z0, Cons(z1, z2)), S(halve#1(length#1(z2))))))
drop#2(0', z0) -> z0
drop#2(S(0'), Nil) -> bot[1]
drop#2(S(z0), Cons(z1, z2)) -> drop#2(z0, z2)
take#2(0', z0) -> Nil
take#2(S(0'), Nil) -> Cons(bot[0], Nil)
take#2(S(z0), Cons(z1, z2)) -> Cons(z1, take#2(z0, z2))
halve#1(0') -> 0'
halve#1(S(0')) -> S(0')
halve#1(S(S(z0))) -> S(halve#1(z0))
const_f#2(z0, Cons(z1, Cons(z2, z3))) -> merge#2(z1, z2)
leq#2(0', z0) -> True
leq#2(S(z0), 0') -> False
leq#2(S(z0), S(z1)) -> leq#2(z0, z1)
length#1(Nil) -> 0'
length#1(Cons(z0, z1)) -> S(length#1(z1))
map#2(dc(z0, z1, z2, z3, z4), Nil) -> Nil
map#2(dc(z0, z1, z2, z3, z4), Cons(z5, z6)) -> Cons(dc#1(z0, z1, z2, z3, z4, z5), map#2(dc(z0, z1, z2, z3, z4), z6))
main(z0) -> dc#1(map, divisible, mergesort_zs_3, divide, const_f, z0)

Types:
DIVIDE_YS#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c:c1
c :: c13:c14:c15 -> c:c1
TAKE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c13:c14:c15
c1 :: c10:c11:c12 -> c:c1
DROP#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c10:c11:c12
COND_MERGE_YS_ZS_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c2:c3
True :: True:False
Cons :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
c2 :: c4:c5:c6 -> c2:c3
MERGE#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c4:c5:c6
False :: True:False
c3 :: c4:c5:c6 -> c2:c3
Nil :: Cons:Nil:S:0':bot[1]:bot[0]
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c2:c3 -> c20:c21:c22 -> c4:c5:c6
leq#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> True:False
LEQ#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c20:c21:c22
DC#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> c7:c8:c9
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c19 -> c25:c26:c27 -> c:c1 -> c16:c17:c18 -> c23:c24 -> c7:c8:c9
CONST_F#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> c19
map#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> dc
divide_ys#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
S :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
halve#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
length#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
MAP#2 :: dc -> Cons:Nil:S:0':bot[1]:bot[0] -> c25:c26:c27
HALVE#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c16:c17:c18
LENGTH#1 :: Cons:Nil:S:0':bot[1]:bot[0] -> c23:c24
0' :: Cons:Nil:S:0':bot[1]:bot[0]
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15
c15 :: c13:c14:c15 -> c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c4:c5:c6 -> c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24
c24 :: c23:c24 -> c23:c24
c25 :: c25:c26:c27
c26 :: c7:c8:c9 -> c25:c26:c27
c27 :: c25:c26:c27 -> c25:c26:c27
MAIN :: Cons:Nil:S:0':bot[1]:bot[0] -> c28
c28 :: c7:c8:c9 -> c28
take#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
drop#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
merge#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
dc#1 :: map -> divisible -> mergesort_zs_3 -> divide -> const_f -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
const_f#2 :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
bot[1] :: Cons:Nil:S:0':bot[1]:bot[0]
bot[0] :: Cons:Nil:S:0':bot[1]:bot[0]
main :: Cons:Nil:S:0':bot[1]:bot[0] -> Cons:Nil:S:0':bot[1]:bot[0]
hole_c:c11_29 :: c:c1
hole_Cons:Nil:S:0':bot[1]:bot[0]2_29 :: Cons:Nil:S:0':bot[1]:bot[0]
hole_c13:c14:c153_29 :: c13:c14:c15
hole_c10:c11:c124_29 :: c10:c11:c12
hole_c2:c35_29 :: c2:c3
hole_True:False6_29 :: True:False
hole_c4:c5:c67_29 :: c4:c5:c6
hole_c20:c21:c228_29 :: c20:c21:c22
hole_c7:c8:c99_29 :: c7:c8:c9
hole_map10_29 :: map
hole_divisible11_29 :: divisible
hole_mergesort_zs_312_29 :: mergesort_zs_3
hole_divide13_29 :: divide
hole_const_f14_29 :: const_f
hole_c1915_29 :: c19
hole_c25:c26:c2716_29 :: c25:c26:c27
hole_c16:c17:c1817_29 :: c16:c17:c18
hole_c23:c2418_29 :: c23:c24
hole_dc19_29 :: dc
hole_c2820_29 :: c28
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29 :: Nat -> Cons:Nil:S:0':bot[1]:bot[0]
gen_c13:c14:c1522_29 :: Nat -> c13:c14:c15
gen_c10:c11:c1223_29 :: Nat -> c10:c11:c12
gen_c20:c21:c2224_29 :: Nat -> c20:c21:c22
gen_c25:c26:c2725_29 :: Nat -> c25:c26:c27
gen_c16:c17:c1826_29 :: Nat -> c16:c17:c18
gen_c23:c2427_29 :: Nat -> c23:c24


Lemmas:
length#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(1, n5083_29))) -> *28_29, rt in Omega(0)
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29)) -> gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n5700_29), rt in Omega(0)
LENGTH#1(gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(n6404_29)) -> gen_c23:c2427_29(n6404_29), rt in Omega(1 + n6404_29)


Generator Equations:
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(0) <=> Nil
gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0':bot[1]:bot[0]21_29(x))
gen_c13:c14:c1522_29(0) <=> c13
gen_c13:c14:c1522_29(+(x, 1)) <=> c15(gen_c13:c14:c1522_29(x))
gen_c10:c11:c1223_29(0) <=> c10
gen_c10:c11:c1223_29(+(x, 1)) <=> c12(gen_c10:c11:c1223_29(x))
gen_c20:c21:c2224_29(0) <=> c20
gen_c20:c21:c2224_29(+(x, 1)) <=> c22(gen_c20:c21:c2224_29(x))
gen_c25:c26:c2725_29(0) <=> c25
gen_c25:c26:c2725_29(+(x, 1)) <=> c27(gen_c25:c26:c2725_29(x))
gen_c16:c17:c1826_29(0) <=> c16
gen_c16:c17:c1826_29(+(x, 1)) <=> c18(gen_c16:c17:c1826_29(x))
gen_c23:c2427_29(0) <=> c23
gen_c23:c2427_29(+(x, 1)) <=> c24(gen_c23:c2427_29(x))


The following defined symbols remain to be analysed:
MAP#2, take#2, drop#2, merge#2