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

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList(@x) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort(@x) → quicksort(testList(#unit))
testQuicksort2(@x) → quicksort(testList(#unit))

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

#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList(@x) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort(@x) → quicksort(testList(#unit))
testQuicksort2(@x) → quicksort(testList(#unit))

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

#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
testList/0
testQuicksort/0
testQuicksort2/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)

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

#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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

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

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#compare, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1, splitD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1
splitD < quicksortD#1
splitD = splitD#1

(8) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1, splitD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1
splitD < quicksortD#1
splitD = splitD#1

(9) 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⁰).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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:
splitD#1, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1
splitD < quicksortD#1
splitD = splitD#1

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

Induction Base:
splitD#1(gen_:::nil7_4(0), gen_#0:#neg:#pos:#s6_4(0)) →_R^Ω(1)
tuple#2(nil, nil)

Induction Step:
splitD#1(gen_:::nil7_4(+(n319016_4, 1)), gen_#0:#neg:#pos:#s6_4(0)) →_R^Ω(1)
splitD#2(splitD(gen_#0:#neg:#pos:#s6_4(0), gen_:::nil7_4(n319016_4)), gen_#0:#neg:#pos:#s6_4(0), #0) →_R^Ω(1)
splitD#2(splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) →_IH
splitD#2(tuple#2(gen_:::nil7_4(c319017_4), gen_:::nil7_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) →_R^Ω(1)
splitD#3(#greater(#0, gen_#0:#neg:#pos:#s6_4(0)), gen_:::nil7_4(n319016_4), gen_:::nil7_4(0), #0) →_R^Ω(1)
splitD#3(#ckgt(#compare(#0, gen_#0:#neg:#pos:#s6_4(0))), gen_:::nil7_4(n319016_4), gen_:::nil7_4(0), #0) →_L^Ω(0)
splitD#3(#ckgt(#EQ), gen_:::nil7_4(n319016_4), gen_:::nil7_4(0), #0) →_R^Ω(0)
splitD#3(#false, gen_:::nil7_4(n319016_4), gen_:::nil7_4(0), #0) →_R^Ω(1)
tuple#2(::(#0, gen_:::nil7_4(n319016_4)), gen_:::nil7_4(0))

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

(13) Complex Obligation (BEST)

(14) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

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:
splitD, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, split#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1
splitD < quicksortD#1
splitD = splitD#1

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(16) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

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:
split#1, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)

Induction Base:
split#1(gen_:::nil7_4(0), gen_#0:#neg:#pos:#s6_4(0)) →_R^Ω(1)
tuple#2(nil, nil)

Induction Step:
split#1(gen_:::nil7_4(+(n321209_4, 1)), gen_#0:#neg:#pos:#s6_4(0)) →_R^Ω(1)
split#2(split(gen_#0:#neg:#pos:#s6_4(0), gen_:::nil7_4(n321209_4)), gen_#0:#neg:#pos:#s6_4(0), #0) →_R^Ω(1)
split#2(split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) →_IH
split#2(tuple#2(gen_:::nil7_4(c321210_4), gen_:::nil7_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) →_R^Ω(1)
split#3(#greater(#0, gen_#0:#neg:#pos:#s6_4(0)), gen_:::nil7_4(n321209_4), gen_:::nil7_4(0), #0) →_R^Ω(1)
split#3(#ckgt(#compare(#0, gen_#0:#neg:#pos:#s6_4(0))), gen_:::nil7_4(n321209_4), gen_:::nil7_4(0), #0) →_L^Ω(0)
split#3(#ckgt(#EQ), gen_:::nil7_4(n321209_4), gen_:::nil7_4(0), #0) →_R^Ω(0)
split#3(#false, gen_:::nil7_4(n321209_4), gen_:::nil7_4(0), #0) →_R^Ω(1)
tuple#2(::(#0, gen_:::nil7_4(n321209_4)), gen_:::nil7_4(0))

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

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)

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:
split, append, append#1, appendD, appendD#1, quicksort, quicksort#1, quicksortD, quicksortD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
split < quicksort#1
split = split#1
quicksortD = quicksortD#1

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

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

(21) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)

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:
appendD#1, append, append#1, appendD, quicksort, quicksort#1, quicksortD, quicksortD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
quicksortD = quicksortD#1

(22) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)

Induction Base:
appendD#1(gen_:::nil7_4(0), gen_:::nil7_4(b)) →_R^Ω(1)
gen_:::nil7_4(b)

Induction Step:
appendD#1(gen_:::nil7_4(+(n323425_4, 1)), gen_:::nil7_4(b)) →_R^Ω(1)
::(#0, appendD(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b))) →_R^Ω(1)
::(#0, appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b))) →_IH
::(#0, gen_:::nil7_4(+(b, c323426_4)))

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

(23) Complex Obligation (BEST)

(24) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)

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:
appendD, append, append#1, quicksort, quicksort#1, quicksortD, quicksortD#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
appendD = appendD#1
appendD < quicksortD#1
quicksort = quicksort#1
quicksortD = quicksortD#1

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(26) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)

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:
quicksortD#1, append, append#1, quicksort, quicksort#1, quicksortD

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
quicksort = quicksort#1
quicksortD = quicksortD#1

(27) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

Induction Base:
quicksortD#1(gen_:::nil7_4(0)) →_R^Ω(1)
nil

Induction Step:
quicksortD#1(gen_:::nil7_4(+(n325184_4, 1))) →_R^Ω(1)
quicksortD#2(splitD(#0, gen_:::nil7_4(n325184_4)), #0) →_R^Ω(1)
quicksortD#2(splitD#1(gen_:::nil7_4(n325184_4), #0), #0) →_L^{Ω(1 + n325184₄)}
quicksortD#2(tuple#2(gen_:::nil7_4(n325184_4), gen_:::nil7_4(0)), #0) →_R^Ω(1)
appendD(quicksortD(gen_:::nil7_4(n325184_4)), ::(#0, quicksortD(gen_:::nil7_4(0)))) →_R^Ω(1)
appendD(quicksortD#1(gen_:::nil7_4(n325184_4)), ::(#0, quicksortD(gen_:::nil7_4(0)))) →_IH
appendD(gen_:::nil7_4(c325185_4), ::(#0, quicksortD(gen_:::nil7_4(0)))) →_R^Ω(1)
appendD(gen_:::nil7_4(n325184_4), ::(#0, quicksortD#1(gen_:::nil7_4(0)))) →_R^Ω(1)
appendD(gen_:::nil7_4(n325184_4), ::(#0, nil)) →_R^Ω(1)
appendD#1(gen_:::nil7_4(n325184_4), ::(#0, nil)) →_L^{Ω(1 + n325184₄)}
gen_:::nil7_4(+(n325184_4, +(0, 1)))

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

(28) Complex Obligation (BEST)

(29) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

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:
quicksortD, append, append#1, quicksort, quicksort#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
quicksort = quicksort#1
quicksortD = quicksortD#1

(30) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(31) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

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:
append#1, append, quicksort, quicksort#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
quicksort = quicksort#1

(32) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)

Induction Base:
append#1(gen_:::nil7_4(0), gen_:::nil7_4(b)) →_R^Ω(1)
gen_:::nil7_4(b)

Induction Step:
append#1(gen_:::nil7_4(+(n326547_4, 1)), gen_:::nil7_4(b)) →_R^Ω(1)
::(#0, append(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b))) →_R^Ω(1)
::(#0, append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b))) →_IH
::(#0, gen_:::nil7_4(+(b, c326548_4)))

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

(33) Complex Obligation (BEST)

(34) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)

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:
append, quicksort, quicksort#1

They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
quicksort = quicksort#1

(35) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(36) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)

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:
quicksort#1, quicksort

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

(37) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quicksort#1(gen_:::nil7_4(n328350_4)) → gen_:::nil7_4(n328350_4), rt ∈ Ω(1 + n328350₄ + n328350₄²)

Induction Base:
quicksort#1(gen_:::nil7_4(0)) →_R^Ω(1)
nil

Induction Step:
quicksort#1(gen_:::nil7_4(+(n328350_4, 1))) →_R^Ω(1)
quicksort#2(split(#0, gen_:::nil7_4(n328350_4)), #0) →_R^Ω(1)
quicksort#2(split#1(gen_:::nil7_4(n328350_4), #0), #0) →_L^{Ω(1 + n328350₄)}
quicksort#2(tuple#2(gen_:::nil7_4(n328350_4), gen_:::nil7_4(0)), #0) →_R^Ω(1)
append(quicksort(gen_:::nil7_4(n328350_4)), ::(#0, quicksort(gen_:::nil7_4(0)))) →_R^Ω(1)
append(quicksort#1(gen_:::nil7_4(n328350_4)), ::(#0, quicksort(gen_:::nil7_4(0)))) →_IH
append(gen_:::nil7_4(c328351_4), ::(#0, quicksort(gen_:::nil7_4(0)))) →_R^Ω(1)
append(gen_:::nil7_4(n328350_4), ::(#0, quicksort#1(gen_:::nil7_4(0)))) →_R^Ω(1)
append(gen_:::nil7_4(n328350_4), ::(#0, nil)) →_R^Ω(1)
append#1(gen_:::nil7_4(n328350_4), ::(#0, nil)) →_L^{Ω(1 + n328350₄)}
gen_:::nil7_4(+(n328350_4, +(0, 1)))

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

(38) Complex Obligation (BEST)

(39) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)
quicksort#1(gen_:::nil7_4(n328350_4)) → gen_:::nil7_4(n328350_4), rt ∈ Ω(1 + n328350₄ + n328350₄²)

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

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

(40) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(41) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)
quicksort#1(gen_:::nil7_4(n328350_4)) → gen_:::nil7_4(n328350_4), rt ∈ Ω(1 + n328350₄ + n328350₄²)

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.

(42) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

(43) BOUNDS(n^2, INF)

(44) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)
quicksort#1(gen_:::nil7_4(n328350_4)) → gen_:::nil7_4(n328350_4), rt ∈ Ω(1 + n328350₄ + n328350₄²)

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.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

(46) BOUNDS(n^2, INF)

(47) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)
append#1(gen_:::nil7_4(n326547_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n326547_4, b)), rt ∈ Ω(1 + n326547₄)

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.

(48) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

(49) BOUNDS(n^2, INF)

(50) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

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.

(51) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
quicksortD#1(gen_:::nil7_4(n325184_4)) → gen_:::nil7_4(n325184_4), rt ∈ Ω(1 + n325184₄ + n325184₄²)

(52) BOUNDS(n^2, INF)

(53) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)
appendD#1(gen_:::nil7_4(n323425_4), gen_:::nil7_4(b)) → gen_:::nil7_4(+(n323425_4, b)), rt ∈ Ω(1 + n323425₄)

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.

(54) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

(55) BOUNDS(n^1, INF)

(56) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)
split#1(gen_:::nil7_4(n321209_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n321209_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n321209₄)

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.

(57) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

(58) BOUNDS(n^1, INF)

(59) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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)
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

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.

(60) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
splitD#1(gen_:::nil7_4(n319016_4), gen_#0:#neg:#pos:#s6_4(0)) → tuple#2(gen_:::nil7_4(n319016_4), gen_:::nil7_4(0)), rt ∈ Ω(1 + n319016₄)

(61) BOUNDS(n^1, INF)

(62) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#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:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#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
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: :::nil
testQuicksort :: :::nil
testQuicksort2 :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s
hole_#false:#true2_4 :: #false:#true
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.

(63) 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)

(64) BOUNDS(1, INF)