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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 261 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 17 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 47 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 1723 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 1512 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 225 ms]
(18) typed CpxTrs
(19) RewriteLemmaProof [LOWER BOUND(ID), 107 ms]
(20) typed CpxTrs
(21) RewriteLemmaProof [LOWER BOUND(ID), 650 ms]
(22) BEST
    (23) proven lower bound
        (24) LowerBoundPropagationProof [FINISHED, 0 ms]
        (25) BOUNDS(n^1, INF)
    (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 534 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 516 ms]
        (30) typed CpxTrs


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

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


The TRS R consists of the following rules:

   #less(@x, @y) -> #cklt(#compare(@x, @y))
   merge(@l1, @l2) -> merge#1(@l1, @l2)
   merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
   merge#1(nil, @l2) -> @l2
   merge#2(::(@y, @ys), @x, @xs) -> merge#3(#less(@x, @y), @x, @xs, @y, @ys)
   merge#2(nil, @x, @xs) -> ::(@x, @xs)
   merge#3(#false, @x, @xs, @y, @ys) -> ::(@y, merge(::(@x, @xs), @ys))
   merge#3(#true, @x, @xs, @y, @ys) -> ::(@x, merge(@xs, ::(@y, @ys)))
   mergesort(@l) -> mergesort#1(@l)
   mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
   mergesort#1(nil) -> nil
   mergesort#2(::(@x2, @xs'), @x1) -> mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
   mergesort#2(nil, @x1) -> ::(@x1, nil)
   mergesort#3(tuple#2(@l1, @l2)) -> merge(mergesort(@l1), mergesort(@l2))
   msplit(@l) -> msplit#1(@l)
   msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
   msplit#1(nil) -> tuple#2(nil, nil)
   msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
   msplit#2(nil, @x1) -> tuple#2(::(@x1, nil), nil)
   msplit#3(tuple#2(@l1, @l2), @x1, @x2) -> tuple#2(::(@x1, @l1), ::(@x2, @l2))

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

   #cklt(#EQ) -> #false
   #cklt(#GT) -> #false
   #cklt(#LT) -> #true
   #compare(#0, #0) -> #EQ
   #compare(#0, #neg(@y)) -> #GT
   #compare(#0, #pos(@y)) -> #LT
   #compare(#0, #s(@y)) -> #LT
   #compare(#neg(@x), #0) -> #LT
   #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
   #compare(#neg(@x), #pos(@y)) -> #LT
   #compare(#pos(@x), #0) -> #GT
   #compare(#pos(@x), #neg(@y)) -> #GT
   #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
   #compare(#s(@x), #0) -> #GT
   #compare(#s(@x), #s(@y)) -> #compare(@x, @y)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

   #less(@x, @y) -> #cklt(#compare(@x, @y))
   merge(@l1, @l2) -> merge#1(@l1, @l2)
   merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
   merge#1(nil, @l2) -> @l2
   merge#2(::(@y, @ys), @x, @xs) -> merge#3(#less(@x, @y), @x, @xs, @y, @ys)
   merge#2(nil, @x, @xs) -> ::(@x, @xs)
   merge#3(#false, @x, @xs, @y, @ys) -> ::(@y, merge(::(@x, @xs), @ys))
   merge#3(#true, @x, @xs, @y, @ys) -> ::(@x, merge(@xs, ::(@y, @ys)))
   mergesort(@l) -> mergesort#1(@l)
   mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
   mergesort#1(nil) -> nil
   mergesort#2(::(@x2, @xs'), @x1) -> mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
   mergesort#2(nil, @x1) -> ::(@x1, nil)
   mergesort#3(tuple#2(@l1, @l2)) -> merge(mergesort(@l1), mergesort(@l2))
   msplit(@l) -> msplit#1(@l)
   msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
   msplit#1(nil) -> tuple#2(nil, nil)
   msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
   msplit#2(nil, @x1) -> tuple#2(::(@x1, nil), nil)
   msplit#3(tuple#2(@l1, @l2), @x1, @x2) -> tuple#2(::(@x1, @l1), ::(@x2, @l2))

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

   #cklt(#EQ) -> #false
   #cklt(#GT) -> #false
   #cklt(#LT) -> #true
   #compare(#0, #0) -> #EQ
   #compare(#0, #neg(@y)) -> #GT
   #compare(#0, #pos(@y)) -> #LT
   #compare(#0, #s(@y)) -> #LT
   #compare(#neg(@x), #0) -> #LT
   #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
   #compare(#neg(@x), #pos(@y)) -> #LT
   #compare(#pos(@x), #0) -> #GT
   #compare(#pos(@x), #neg(@y)) -> #GT
   #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
   #compare(#s(@x), #0) -> #GT
   #compare(#s(@x), #s(@y)) -> #compare(@x, @y)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #cklt(#EQ) -> #false
   #cklt(#GT) -> #false
   #cklt(#LT) -> #true
   #compare(#0, #0) -> #EQ
   #compare(#0, #neg(z0)) -> #GT
   #compare(#0, #pos(z0)) -> #LT
   #compare(#0, #s(z0)) -> #LT
   #compare(#neg(z0), #0) -> #LT
   #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
   #compare(#neg(z0), #pos(z1)) -> #LT
   #compare(#pos(z0), #0) -> #GT
   #compare(#pos(z0), #neg(z1)) -> #GT
   #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
   #compare(#s(z0), #0) -> #GT
   #compare(#s(z0), #s(z1)) -> #compare(z0, z1)
   #less(z0, z1) -> #cklt(#compare(z0, z1))
   merge(z0, z1) -> merge#1(z0, z1)
   merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
   merge#1(nil, z0) -> z0
   merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
   merge#2(nil, z0, z1) -> ::(z0, z1)
   merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
   merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
   mergesort(z0) -> mergesort#1(z0)
   mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
   mergesort#1(nil) -> nil
   mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
   mergesort#2(nil, z0) -> ::(z0, nil)
   mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
   msplit(z0) -> msplit#1(z0)
   msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
   msplit#1(nil) -> tuple#2(nil, nil)
   msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
   msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
   msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))
Tuples:
   #CKLT(#EQ) -> c
   #CKLT(#GT) -> c1
   #CKLT(#LT) -> c2
   #COMPARE(#0, #0) -> c3
   #COMPARE(#0, #neg(z0)) -> c4
   #COMPARE(#0, #pos(z0)) -> c5
   #COMPARE(#0, #s(z0)) -> c6
   #COMPARE(#neg(z0), #0) -> c7
   #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
   #COMPARE(#neg(z0), #pos(z1)) -> c9
   #COMPARE(#pos(z0), #0) -> c10
   #COMPARE(#pos(z0), #neg(z1)) -> c11
   #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
   #COMPARE(#s(z0), #0) -> c13
   #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
   #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
   MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
   MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
   MERGE#1(nil, z0) -> c18
   MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
   MERGE#2(nil, z0, z1) -> c20
   MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
   MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
   MERGESORT(z0) -> c23(MERGESORT#1(z0))
   MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
   MERGESORT#1(nil) -> c25
   MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
   MERGESORT#2(nil, z0) -> c27
   MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
   MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
   MSPLIT(z0) -> c30(MSPLIT#1(z0))
   MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
   MSPLIT#1(nil) -> c32
   MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
   MSPLIT#2(nil, z0) -> c34
   MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
S tuples:
   #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
   MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
   MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
   MERGE#1(nil, z0) -> c18
   MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
   MERGE#2(nil, z0, z1) -> c20
   MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
   MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
   MERGESORT(z0) -> c23(MERGESORT#1(z0))
   MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
   MERGESORT#1(nil) -> c25
   MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
   MERGESORT#2(nil, z0) -> c27
   MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
   MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
   MSPLIT(z0) -> c30(MSPLIT#1(z0))
   MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
   MSPLIT#1(nil) -> c32
   MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
   MSPLIT#2(nil, z0) -> c34
   MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
K tuples:none
Defined Rule Symbols:   #less_2, merge_2, merge#1_2, merge#2_3, merge#3_5, mergesort_1, mergesort#1_1, mergesort#2_2, mergesort#3_1, msplit_1, msplit#1_1, msplit#2_2, msplit#3_3, #cklt_1, #compare_2

Defined Pair Symbols:   #CKLT_1, #COMPARE_2, #LESS_2, MERGE_2, MERGE#1_2, MERGE#2_3, MERGE#3_5, MERGESORT_1, MERGESORT#1_1, MERGESORT#2_2, MERGESORT#3_1, MSPLIT_1, MSPLIT#1_1, MSPLIT#2_2, MSPLIT#3_3

Compound Symbols:   c, c1, c2, c3, c4, c5, c6, c7, c8_1, c9, c10, c11, c12_1, c13, c14_1, c15_2, c16_1, c17_1, c18, c19_2, c20, c21_1, c22_1, c23_1, c24_1, c25, c26_2, c27, c28_2, c29_2, c30_1, c31_1, c32, c33_2, c34, c35


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

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

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

   #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
   MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
   MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
   MERGE#1(nil, z0) -> c18
   MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
   MERGE#2(nil, z0, z1) -> c20
   MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
   MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
   MERGESORT(z0) -> c23(MERGESORT#1(z0))
   MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
   MERGESORT#1(nil) -> c25
   MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
   MERGESORT#2(nil, z0) -> c27
   MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
   MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
   MSPLIT(z0) -> c30(MSPLIT#1(z0))
   MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
   MSPLIT#1(nil) -> c32
   MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
   MSPLIT#2(nil, z0) -> c34
   MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35

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

   #CKLT(#EQ) -> c
   #CKLT(#GT) -> c1
   #CKLT(#LT) -> c2
   #COMPARE(#0, #0) -> c3
   #COMPARE(#0, #neg(z0)) -> c4
   #COMPARE(#0, #pos(z0)) -> c5
   #COMPARE(#0, #s(z0)) -> c6
   #COMPARE(#neg(z0), #0) -> c7
   #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
   #COMPARE(#neg(z0), #pos(z1)) -> c9
   #COMPARE(#pos(z0), #0) -> c10
   #COMPARE(#pos(z0), #neg(z1)) -> c11
   #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
   #COMPARE(#s(z0), #0) -> c13
   #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
   #cklt(#EQ) -> #false
   #cklt(#GT) -> #false
   #cklt(#LT) -> #true
   #compare(#0, #0) -> #EQ
   #compare(#0, #neg(z0)) -> #GT
   #compare(#0, #pos(z0)) -> #LT
   #compare(#0, #s(z0)) -> #LT
   #compare(#neg(z0), #0) -> #LT
   #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
   #compare(#neg(z0), #pos(z1)) -> #LT
   #compare(#pos(z0), #0) -> #GT
   #compare(#pos(z0), #neg(z1)) -> #GT
   #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
   #compare(#s(z0), #0) -> #GT
   #compare(#s(z0), #s(z1)) -> #compare(z0, z1)
   #less(z0, z1) -> #cklt(#compare(z0, z1))
   merge(z0, z1) -> merge#1(z0, z1)
   merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
   merge#1(nil, z0) -> z0
   merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
   merge#2(nil, z0, z1) -> ::(z0, z1)
   merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
   merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
   mergesort(z0) -> mergesort#1(z0)
   mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
   mergesort#1(nil) -> nil
   mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
   mergesort#2(nil, z0) -> ::(z0, nil)
   mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
   msplit(z0) -> msplit#1(z0)
   msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
   msplit#1(nil) -> tuple#2(nil, nil)
   msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
   msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
   msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

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

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

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

   #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
   MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
   MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
   MERGE#1(nil, z0) -> c18
   MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
   MERGE#2(nil, z0, z1) -> c20
   MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
   MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
   MERGESORT(z0) -> c23(MERGESORT#1(z0))
   MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
   MERGESORT#1(nil) -> c25
   MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
   MERGESORT#2(nil, z0) -> c27
   MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
   MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
   MSPLIT(z0) -> c30(MSPLIT#1(z0))
   MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
   MSPLIT#1(nil) -> c32
   MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
   MSPLIT#2(nil, z0) -> c34
   MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35

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

   #CKLT(#EQ) -> c
   #CKLT(#GT) -> c1
   #CKLT(#LT) -> c2
   #COMPARE(#0, #0) -> c3
   #COMPARE(#0, #neg(z0)) -> c4
   #COMPARE(#0, #pos(z0)) -> c5
   #COMPARE(#0, #s(z0)) -> c6
   #COMPARE(#neg(z0), #0) -> c7
   #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
   #COMPARE(#neg(z0), #pos(z1)) -> c9
   #COMPARE(#pos(z0), #0) -> c10
   #COMPARE(#pos(z0), #neg(z1)) -> c11
   #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
   #COMPARE(#s(z0), #0) -> c13
   #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
   #cklt(#EQ) -> #false
   #cklt(#GT) -> #false
   #cklt(#LT) -> #true
   #compare(#0, #0) -> #EQ
   #compare(#0, #neg(z0)) -> #GT
   #compare(#0, #pos(z0)) -> #LT
   #compare(#0, #s(z0)) -> #LT
   #compare(#neg(z0), #0) -> #LT
   #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
   #compare(#neg(z0), #pos(z1)) -> #LT
   #compare(#pos(z0), #0) -> #GT
   #compare(#pos(z0), #neg(z1)) -> #GT
   #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
   #compare(#s(z0), #0) -> #GT
   #compare(#s(z0), #s(z1)) -> #compare(z0, z1)
   #less(z0, z1) -> #cklt(#compare(z0, z1))
   merge(z0, z1) -> merge#1(z0, z1)
   merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
   merge#1(nil, z0) -> z0
   merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
   merge#2(nil, z0, z1) -> ::(z0, z1)
   merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
   merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
   mergesort(z0) -> mergesort#1(z0)
   mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
   mergesort#1(nil) -> nil
   mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
   mergesort#2(nil, z0) -> ::(z0, nil)
   mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
   msplit(z0) -> msplit#1(z0)
   msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
   msplit#1(nil) -> tuple#2(nil, nil)
   msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
   msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
   msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

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

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

(10)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
#compare, #COMPARE, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, msplit, MSPLIT, mergesort, MSPLIT#1, merge, merge#1, mergesort#1, mergesort#3, msplit#1

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
merge = merge#1
merge < mergesort#3
mergesort#1 = mergesort#3

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

(12)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
#compare, #COMPARE, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, msplit, MSPLIT, mergesort, MSPLIT#1, merge, merge#1, mergesort#1, mergesort#3, msplit#1

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
merge = merge#1
merge < mergesort#3
mergesort#1 = mergesort#3

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s21_36(0), gen_#0:#neg:#pos:#s21_36(0)) ->_R^Omega(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s21_36(+(n25_36, 1)), gen_#0:#neg:#pos:#s21_36(+(n25_36, 1))) ->_R^Omega(0)
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) ->_IH
#EQ

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:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
#COMPARE, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, msplit, MSPLIT, mergesort, MSPLIT#1, merge, merge#1, mergesort#1, mergesort#3, msplit#1

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
merge = merge#1
merge < mergesort#3
mergesort#1 = mergesort#3

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)

Induction Base:
#COMPARE(gen_#0:#neg:#pos:#s21_36(0), gen_#0:#neg:#pos:#s21_36(0)) ->_R^Omega(0)
c3

Induction Step:
#COMPARE(gen_#0:#neg:#pos:#s21_36(+(n318940_36, 1)), gen_#0:#neg:#pos:#s21_36(+(n318940_36, 1))) ->_R^Omega(0)
c8(#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36))) ->_IH
c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(c318941_36))

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

(16)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
merge#1, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, msplit, MSPLIT, mergesort, MSPLIT#1, merge, mergesort#1, mergesort#3, msplit#1

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
merge = merge#1
merge < mergesort#3
mergesort#1 = mergesort#3

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)

Induction Base:
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(0)) ->_R^Omega(0)
merge#2(gen_:::nil23_36(0), #0, gen_:::nil23_36(0)) ->_R^Omega(0)
::(#0, gen_:::nil23_36(0))

Induction Step:
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(+(n638265_36, 1))) ->_R^Omega(0)
merge#2(gen_:::nil23_36(+(n638265_36, 1)), #0, gen_:::nil23_36(0)) ->_R^Omega(0)
merge#3(#less(#0, #0), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n638265_36)) ->_R^Omega(0)
merge#3(#cklt(#compare(#0, #0)), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n638265_36)) ->_L^Omega(0)
merge#3(#cklt(#EQ), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n638265_36)) ->_R^Omega(0)
merge#3(#false, #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n638265_36)) ->_R^Omega(0)
::(#0, merge(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n638265_36))) ->_R^Omega(0)
::(#0, merge#1(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n638265_36))) ->_IH
::(#0, gen_:::nil23_36(+(1, c638266_36)))

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

(18)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
merge, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, msplit, MSPLIT, mergesort, MSPLIT#1, mergesort#1, mergesort#3, msplit#1

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
merge = merge#1
merge < mergesort#3
mergesort#1 = mergesort#3

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)

Induction Base:
msplit#1(gen_:::nil23_36(*(2, 0))) ->_R^Omega(0)
tuple#2(nil, nil)

Induction Step:
msplit#1(gen_:::nil23_36(*(2, +(n641797_36, 1)))) ->_R^Omega(0)
msplit#2(gen_:::nil23_36(+(1, *(2, n641797_36))), #0) ->_R^Omega(0)
msplit#3(msplit(gen_:::nil23_36(*(2, n641797_36))), #0, #0) ->_R^Omega(0)
msplit#3(msplit#1(gen_:::nil23_36(*(2, n641797_36))), #0, #0) ->_IH
msplit#3(tuple#2(gen_:::nil23_36(c641798_36), gen_:::nil23_36(c641798_36)), #0, #0) ->_R^Omega(0)
tuple#2(::(#0, gen_:::nil23_36(n641797_36)), ::(#0, gen_:::nil23_36(n641797_36)))

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

(20)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
msplit, MERGE, MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3, MSPLIT, mergesort, MSPLIT#1, mergesort#1, mergesort#3

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3
msplit < MERGESORT#1
MSPLIT < MERGESORT#1
mergesort < MERGESORT#3
msplit < MSPLIT#1
msplit < mergesort#1
msplit = msplit#1
MSPLIT = MSPLIT#1
mergesort = mergesort#1
mergesort = mergesort#3
mergesort#1 = mergesort#3

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(n643970_36)) -> *24_36, rt in Omega(n643970_36)

Induction Base:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(0))

Induction Step:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(+(n643970_36, 1))) ->_R^Omega(1)
c17(MERGE#2(gen_:::nil23_36(+(n643970_36, 1)), #0, gen_:::nil23_36(0))) ->_R^Omega(1)
c17(c19(MERGE#3(#less(#0, #0), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n643970_36)), #LESS(#0, #0))) ->_R^Omega(0)
c17(c19(MERGE#3(#cklt(#compare(#0, #0)), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n643970_36)), #LESS(#0, #0))) ->_L^Omega(0)
c17(c19(MERGE#3(#cklt(#EQ), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n643970_36)), #LESS(#0, #0))) ->_R^Omega(0)
c17(c19(MERGE#3(#false, #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n643970_36)), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(MERGE(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n643970_36))), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(c16(MERGE#1(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n643970_36)))), #LESS(#0, #0))) ->_IH
c17(c19(c21(c16(*24_36)), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(c16(*24_36)), c15(#CKLT(#compare(#0, #0)), #COMPARE(#0, #0)))) ->_L^Omega(0)
c17(c19(c21(c16(*24_36)), c15(#CKLT(#EQ), #COMPARE(#0, #0)))) ->_R^Omega(0)
c17(c19(c21(c16(*24_36)), c15(c, #COMPARE(#0, #0)))) ->_L^Omega(0)
c17(c19(c21(c16(*24_36)), c15(c, gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0))))

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

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
MERGE#1, MERGE, MERGESORT, MERGESORT#1, MERGESORT#3

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3

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

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(n643970_36)) -> *24_36, rt in Omega(n643970_36)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
MERGE, MERGESORT, MERGESORT#1, MERGESORT#3

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MERGE(gen_:::nil23_36(1), gen_:::nil23_36(n650714_36)) -> *24_36, rt in Omega(n650714_36)

Induction Base:
MERGE(gen_:::nil23_36(1), gen_:::nil23_36(0))

Induction Step:
MERGE(gen_:::nil23_36(1), gen_:::nil23_36(+(n650714_36, 1))) ->_R^Omega(1)
c16(MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(+(n650714_36, 1)))) ->_R^Omega(1)
c16(c17(MERGE#2(gen_:::nil23_36(+(1, n650714_36)), #0, gen_:::nil23_36(0)))) ->_R^Omega(1)
c16(c17(c19(MERGE#3(#less(#0, #0), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n650714_36)), #LESS(#0, #0)))) ->_R^Omega(0)
c16(c17(c19(MERGE#3(#cklt(#compare(#0, #0)), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n650714_36)), #LESS(#0, #0)))) ->_L^Omega(0)
c16(c17(c19(MERGE#3(#cklt(#EQ), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n650714_36)), #LESS(#0, #0)))) ->_R^Omega(0)
c16(c17(c19(MERGE#3(#false, #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n650714_36)), #LESS(#0, #0)))) ->_R^Omega(1)
c16(c17(c19(c21(MERGE(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n650714_36))), #LESS(#0, #0)))) ->_IH
c16(c17(c19(c21(*24_36), #LESS(#0, #0)))) ->_R^Omega(1)
c16(c17(c19(c21(*24_36), c15(#CKLT(#compare(#0, #0)), #COMPARE(#0, #0))))) ->_L^Omega(0)
c16(c17(c19(c21(*24_36), c15(#CKLT(#EQ), #COMPARE(#0, #0))))) ->_R^Omega(0)
c16(c17(c19(c21(*24_36), c15(c, #COMPARE(#0, #0))))) ->_L^Omega(0)
c16(c17(c19(c21(*24_36), c15(c, gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0)))))

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

(28)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(n643970_36)) -> *24_36, rt in Omega(n643970_36)
MERGE(gen_:::nil23_36(1), gen_:::nil23_36(n650714_36)) -> *24_36, rt in Omega(n650714_36)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
MERGE#1, MERGESORT, MERGESORT#1, MERGESORT#3

They will be analysed ascendingly in the following order:
MERGE = MERGE#1
MERGE < MERGESORT#3
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(n658759_36)) -> *24_36, rt in Omega(n658759_36)

Induction Base:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(0))

Induction Step:
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(+(n658759_36, 1))) ->_R^Omega(1)
c17(MERGE#2(gen_:::nil23_36(+(n658759_36, 1)), #0, gen_:::nil23_36(0))) ->_R^Omega(1)
c17(c19(MERGE#3(#less(#0, #0), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n658759_36)), #LESS(#0, #0))) ->_R^Omega(0)
c17(c19(MERGE#3(#cklt(#compare(#0, #0)), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n658759_36)), #LESS(#0, #0))) ->_L^Omega(0)
c17(c19(MERGE#3(#cklt(#EQ), #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n658759_36)), #LESS(#0, #0))) ->_R^Omega(0)
c17(c19(MERGE#3(#false, #0, gen_:::nil23_36(0), #0, gen_:::nil23_36(n658759_36)), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(MERGE(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n658759_36))), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(c16(MERGE#1(::(#0, gen_:::nil23_36(0)), gen_:::nil23_36(n658759_36)))), #LESS(#0, #0))) ->_IH
c17(c19(c21(c16(*24_36)), #LESS(#0, #0))) ->_R^Omega(1)
c17(c19(c21(c16(*24_36)), c15(#CKLT(#compare(#0, #0)), #COMPARE(#0, #0)))) ->_L^Omega(0)
c17(c19(c21(c16(*24_36)), c15(#CKLT(#EQ), #COMPARE(#0, #0)))) ->_R^Omega(0)
c17(c19(c21(c16(*24_36)), c15(c, #COMPARE(#0, #0)))) ->_L^Omega(0)
c17(c19(c21(c16(*24_36)), c15(c, gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0))))

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

(30)
Obligation:
Innermost TRS:
Rules:
#LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
MERGE(z0, z1) -> c16(MERGE#1(z0, z1))
MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1))
MERGE#1(nil, z0) -> c18
MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0))
MERGE#2(nil, z0, z1) -> c20
MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3))
MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3)))
MERGESORT(z0) -> c23(MERGESORT#1(z0))
MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0))
MERGESORT#1(nil) -> c25
MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1))))
MERGESORT#2(nil, z0) -> c27
MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0))
MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1))
MSPLIT(z0) -> c30(MSPLIT#1(z0))
MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0))
MSPLIT#1(nil) -> c32
MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1))
MSPLIT#2(nil, z0) -> c34
MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35
#CKLT(#EQ) -> c
#CKLT(#GT) -> c1
#CKLT(#LT) -> c2
#COMPARE(#0, #0) -> c3
#COMPARE(#0, #neg(z0)) -> c4
#COMPARE(#0, #pos(z0)) -> c5
#COMPARE(#0, #s(z0)) -> c6
#COMPARE(#neg(z0), #0) -> c7
#COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) -> c9
#COMPARE(#pos(z0), #0) -> c10
#COMPARE(#pos(z0), #neg(z1)) -> c11
#COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) -> c13
#COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1))
#cklt(#EQ) -> #false
#cklt(#GT) -> #false
#cklt(#LT) -> #true
#compare(#0, #0) -> #EQ
#compare(#0, #neg(z0)) -> #GT
#compare(#0, #pos(z0)) -> #LT
#compare(#0, #s(z0)) -> #LT
#compare(#neg(z0), #0) -> #LT
#compare(#neg(z0), #neg(z1)) -> #compare(z1, z0)
#compare(#neg(z0), #pos(z1)) -> #LT
#compare(#pos(z0), #0) -> #GT
#compare(#pos(z0), #neg(z1)) -> #GT
#compare(#pos(z0), #pos(z1)) -> #compare(z0, z1)
#compare(#s(z0), #0) -> #GT
#compare(#s(z0), #s(z1)) -> #compare(z0, z1)
#less(z0, z1) -> #cklt(#compare(z0, z1))
merge(z0, z1) -> merge#1(z0, z1)
merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1)
merge#1(nil, z0) -> z0
merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1)
merge#2(nil, z0, z1) -> ::(z0, z1)
merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3))
merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3)))
mergesort(z0) -> mergesort#1(z0)
mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0)
mergesort#1(nil) -> nil
mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1))))
mergesort#2(nil, z0) -> ::(z0, nil)
mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1))
msplit(z0) -> msplit#1(z0)
msplit#1(::(z0, z1)) -> msplit#2(z1, z0)
msplit#1(nil) -> tuple#2(nil, nil)
msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0)
msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil)
msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1))

Types:
#LESS :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c15
c15 :: c:c1:c2 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c15
#CKLT :: #EQ:#GT:#LT -> c:c1:c2
#compare :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #EQ:#GT:#LT
#COMPARE :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
MERGE :: :::nil -> :::nil -> c16
c16 :: c17:c18 -> c16
MERGE#1 :: :::nil -> :::nil -> c17:c18
:: :: #0:#neg:#pos:#s -> :::nil -> :::nil
c17 :: c19:c20 -> c17:c18
MERGE#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> c19:c20
nil :: :::nil
c18 :: c17:c18
c19 :: c21:c22 -> c15 -> c19:c20
MERGE#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> c21:c22
#less :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> #false:#true
c20 :: c19:c20
#false :: #false:#true
c21 :: c16 -> c21:c22
#true :: #false:#true
c22 :: c16 -> c21:c22
MERGESORT :: :::nil -> c23
c23 :: c24:c25 -> c23
MERGESORT#1 :: :::nil -> c24:c25
c24 :: c26:c27 -> c24:c25
MERGESORT#2 :: :::nil -> #0:#neg:#pos:#s -> c26:c27
c25 :: c24:c25
c26 :: c28:c29 -> c30 -> c26:c27
MERGESORT#3 :: tuple#2 -> c28:c29
msplit :: :::nil -> tuple#2
MSPLIT :: :::nil -> c30
c27 :: c26:c27
tuple#2 :: :::nil -> :::nil -> tuple#2
c28 :: c16 -> c23 -> c28:c29
mergesort :: :::nil -> :::nil
c29 :: c16 -> c23 -> c28:c29
c30 :: c31:c32 -> c30
MSPLIT#1 :: :::nil -> c31:c32
c31 :: c33:c34 -> c31:c32
MSPLIT#2 :: :::nil -> #0:#neg:#pos:#s -> c33:c34
c32 :: c31:c32
c33 :: c35 -> c30 -> c33:c34
MSPLIT#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> c35
c34 :: c33:c34
c35 :: c35
#EQ :: #EQ:#GT:#LT
c :: c:c1:c2
#GT :: #EQ:#GT:#LT
c1 :: c:c1:c2
#LT :: #EQ:#GT:#LT
c2 :: c:c1:c2
#0 :: #0:#neg:#pos:#s
c3 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#neg :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c4 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#pos :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c5 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#s :: #0:#neg:#pos:#s -> #0:#neg:#pos:#s
c6 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c7 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c8 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c9 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c10 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c11 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c12 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c13 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
c14 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14 -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
#cklt :: #EQ:#GT:#LT -> #false:#true
merge :: :::nil -> :::nil -> :::nil
merge#1 :: :::nil -> :::nil -> :::nil
merge#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
merge#3 :: #false:#true -> #0:#neg:#pos:#s -> :::nil -> #0:#neg:#pos:#s -> :::nil -> :::nil
mergesort#1 :: :::nil -> :::nil
mergesort#2 :: :::nil -> #0:#neg:#pos:#s -> :::nil
mergesort#3 :: tuple#2 -> :::nil
msplit#1 :: :::nil -> tuple#2
msplit#2 :: :::nil -> #0:#neg:#pos:#s -> tuple#2
msplit#3 :: tuple#2 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2
hole_c151_36 :: c15
hole_#0:#neg:#pos:#s2_36 :: #0:#neg:#pos:#s
hole_c:c1:c23_36 :: c:c1:c2
hole_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c144_36 :: c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
hole_#EQ:#GT:#LT5_36 :: #EQ:#GT:#LT
hole_c166_36 :: c16
hole_:::nil7_36 :: :::nil
hole_c17:c188_36 :: c17:c18
hole_c19:c209_36 :: c19:c20
hole_c21:c2210_36 :: c21:c22
hole_#false:#true11_36 :: #false:#true
hole_c2312_36 :: c23
hole_c24:c2513_36 :: c24:c25
hole_c26:c2714_36 :: c26:c27
hole_c28:c2915_36 :: c28:c29
hole_c3016_36 :: c30
hole_tuple#217_36 :: tuple#2
hole_c31:c3218_36 :: c31:c32
hole_c33:c3419_36 :: c33:c34
hole_c3520_36 :: c35
gen_#0:#neg:#pos:#s21_36 :: Nat -> #0:#neg:#pos:#s
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36 :: Nat -> c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c14
gen_:::nil23_36 :: Nat -> :::nil


Lemmas:
#compare(gen_#0:#neg:#pos:#s21_36(n25_36), gen_#0:#neg:#pos:#s21_36(n25_36)) -> #EQ, rt in Omega(0)
#COMPARE(gen_#0:#neg:#pos:#s21_36(n318940_36), gen_#0:#neg:#pos:#s21_36(n318940_36)) -> gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(n318940_36), rt in Omega(0)
merge#1(gen_:::nil23_36(1), gen_:::nil23_36(n638265_36)) -> gen_:::nil23_36(+(1, n638265_36)), rt in Omega(0)
msplit#1(gen_:::nil23_36(*(2, n641797_36))) -> tuple#2(gen_:::nil23_36(n641797_36), gen_:::nil23_36(n641797_36)), rt in Omega(0)
MERGE#1(gen_:::nil23_36(1), gen_:::nil23_36(n658759_36)) -> *24_36, rt in Omega(n658759_36)
MERGE(gen_:::nil23_36(1), gen_:::nil23_36(n650714_36)) -> *24_36, rt in Omega(n650714_36)


Generator Equations:
gen_#0:#neg:#pos:#s21_36(0) <=> #0
gen_#0:#neg:#pos:#s21_36(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s21_36(x))
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(0) <=> c3
gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(+(x, 1)) <=> c8(gen_c3:c4:c5:c6:c7:c8:c9:c10:c11:c12:c13:c1422_36(x))
gen_:::nil23_36(0) <=> nil
gen_:::nil23_36(+(x, 1)) <=> ::(#0, gen_:::nil23_36(x))


The following defined symbols remain to be analysed:
MERGESORT#1, MERGESORT, MERGESORT#3

They will be analysed ascendingly in the following order:
MERGESORT = MERGESORT#1
MERGESORT = MERGESORT#3
MERGESORT#1 = MERGESORT#3