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

(0) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#compare, merge, merge#1, mergesort, mergesort#1, mergesort#3, msplit, 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 = msplit#1

(6) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

The following defined symbols remain to be analysed:
#compare, merge, merge#1, mergesort, mergesort#1, mergesort#3, msplit, 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 = msplit#1

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s6_4(0), gen_#0:#neg:#pos:#s6_4(0)) →_R^Ω(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s6_4(+(n9_4, 1)), gen_#0:#neg:#pos:#s6_4(+(n9_4, 1))) →_R^Ω(0)
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) →_IH
#EQ

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(8) Complex Obligation (BEST)

(9) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

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

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 = msplit#1

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

Induction Base:
msplit#1(gen_:::nil7_4(*(2, 0))) →_R^Ω(1)
tuple#2(nil, nil)

Induction Step:
msplit#1(gen_:::nil7_4(*(2, +(n318908_4, 1)))) →_R^Ω(1)
msplit#2(gen_:::nil7_4(+(1, *(2, n318908_4))), #0) →_R^Ω(1)
msplit#3(msplit(gen_:::nil7_4(*(2, n318908_4))), #0, #0) →_R^Ω(1)
msplit#3(msplit#1(gen_:::nil7_4(*(2, n318908_4))), #0, #0) →_IH
msplit#3(tuple#2(gen_:::nil7_4(c318909_4), gen_:::nil7_4(c318909_4)), #0, #0) →_R^Ω(1)
tuple#2(::(#0, gen_:::nil7_4(n318908_4)), ::(#0, gen_:::nil7_4(n318908_4)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

The following defined symbols remain to be analysed:
msplit, merge, 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
msplit < mergesort#1
msplit = msplit#1

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol msplit.

(14) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(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

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Induction Base:
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(0)) →_R^Ω(1)
merge#2(gen_:::nil7_4(0), #0, gen_:::nil7_4(0)) →_R^Ω(1)
::(#0, gen_:::nil7_4(0))

Induction Step:
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(+(n319802_4, 1))) →_R^Ω(1)
merge#2(gen_:::nil7_4(+(n319802_4, 1)), #0, gen_:::nil7_4(0)) →_R^Ω(1)
merge#3(#less(#0, #0), #0, gen_:::nil7_4(0), #0, gen_:::nil7_4(n319802_4)) →_R^Ω(1)
merge#3(#cklt(#compare(#0, #0)), #0, gen_:::nil7_4(0), #0, gen_:::nil7_4(n319802_4)) →_L^Ω(0)
merge#3(#cklt(#EQ), #0, gen_:::nil7_4(0), #0, gen_:::nil7_4(n319802_4)) →_R^Ω(0)
merge#3(#false, #0, gen_:::nil7_4(0), #0, gen_:::nil7_4(n319802_4)) →_R^Ω(1)
::(#0, merge(::(#0, gen_:::nil7_4(0)), gen_:::nil7_4(n319802_4))) →_R^Ω(1)
::(#0, merge#1(::(#0, gen_:::nil7_4(0)), gen_:::nil7_4(n319802_4))) →_IH
::(#0, gen_:::nil7_4(+(1, c319803_4)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(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

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol merge.

(19) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(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

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mergesort#1.

(21) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

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

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

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mergesort#3.

(23) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

The following defined symbols remain to be analysed:
mergesort

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

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mergesort.

(25) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

(27) BOUNDS(n^1, INF)

(28) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)
merge#1(gen_:::nil7_4(1), gen_:::nil7_4(n319802_4)) → gen_:::nil7_4(+(1, n319802_4)), rt ∈ Ω(1 + n319802₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

(30) BOUNDS(n^1, INF)

(31) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
msplit#1(gen_:::nil7_4(*(2, n318908_4))) → tuple#2(gen_:::nil7_4(n318908_4), gen_:::nil7_4(n318908_4)), rt ∈ Ω(1 + n318908₄)

(33) BOUNDS(n^1, INF)

(34) Obligation:

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

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
merge :: :::nil → :::nil → :::nil
merge#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
merge#2 :: :::nil → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
merge#3 :: #false:#true → #0:#neg:#pos:#s → :::nil → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
mergesort :: :::nil → :::nil
mergesort#1 :: :::nil → :::nil
mergesort#2 :: :::nil → #0:#neg:#pos:#s → :::nil
mergesort#3 :: tuple#2 → :::nil
msplit :: :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
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
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
hole_tuple#25_4 :: tuple#2
gen_#0:#neg:#pos:#s6_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_4(0) ⇔ #0
gen_#0:#neg:#pos:#s6_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_4(x))
gen_:::nil7_4(0) ⇔ nil
gen_:::nil7_4(+(x, 1)) ⇔ ::(#0, gen_:::nil7_4(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) → #EQ, rt ∈ Ω(0)

(36) BOUNDS(1, INF)