WORST_CASE(Omega(n^1),?)
proof of input_9eGVsIEx4Y.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 57 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 43 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 350 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 86 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 126 ms]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 49 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (24) typed CpxTrs


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

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


The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   qsort(z0) -> qs(half(length(z0)), z0)
   qs(z0, nil) -> nil
   qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
   filterlow(z0, nil) -> nil
   filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> filterlow(z0, z2)
   if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
   filterhigh(z0, nil) -> nil
   filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
   if2(true, z0, z1, z2) -> filterhigh(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   append(nil, ys) -> ys
   append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   get(z0, nil) -> 0
   get(z0, cons(z1, nil)) -> z1
   get(0, cons(z0, cons(z1, z2))) -> z0
   get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))
Tuples:
   QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
   QS(z0, nil) -> c1
   QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   FILTERLOW(z0, nil) -> c7
   FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c11
   FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   APPEND(nil, ys) -> c18
   APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
   LENGTH(nil) -> c20
   LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
   HALF(0) -> c22
   HALF(s(0)) -> c23
   HALF(s(s(z0))) -> c24(HALF(z0))
   GET(z0, nil) -> c25
   GET(z0, cons(z1, nil)) -> c26
   GET(0, cons(z0, cons(z1, z2))) -> c27
   GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
S tuples:
   QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
   QS(z0, nil) -> c1
   QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   FILTERLOW(z0, nil) -> c7
   FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c11
   FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   APPEND(nil, ys) -> c18
   APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
   LENGTH(nil) -> c20
   LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
   HALF(0) -> c22
   HALF(s(0)) -> c23
   HALF(s(s(z0))) -> c24(HALF(z0))
   GET(z0, nil) -> c25
   GET(z0, cons(z1, nil)) -> c26
   GET(0, cons(z0, cons(z1, z2))) -> c27
   GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
K tuples:none
Defined Rule Symbols:   qsort_1, qs_2, filterlow_2, if1_4, filterhigh_2, if2_4, ge_2, append_2, length_1, half_1, get_2

Defined Pair Symbols:   QSORT_1, QS_2, FILTERLOW_2, IF1_4, FILTERHIGH_2, IF2_4, GE_2, APPEND_2, LENGTH_1, HALF_1, GET_2

Compound Symbols:   c_3, c1, c2_3, c3_4, c4_2, c5_3, c6_4, c7, c8_2, c9_1, c10_1, c11, c12_2, c13_1, c14_1, c15, c16, c17_1, c18, c19_1, c20, c21_1, c22, c23, c24_1, c25, c26, c27, c28_1


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

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

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


The TRS R consists of the following rules:

   QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
   QS(z0, nil) -> c1
   QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   FILTERLOW(z0, nil) -> c7
   FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c11
   FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   APPEND(nil, ys) -> c18
   APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
   LENGTH(nil) -> c20
   LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
   HALF(0) -> c22
   HALF(s(0)) -> c23
   HALF(s(s(z0))) -> c24(HALF(z0))
   GET(z0, nil) -> c25
   GET(z0, cons(z1, nil)) -> c26
   GET(0, cons(z0, cons(z1, z2))) -> c27
   GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))

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

   qsort(z0) -> qs(half(length(z0)), z0)
   qs(z0, nil) -> nil
   qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
   filterlow(z0, nil) -> nil
   filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> filterlow(z0, z2)
   if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
   filterhigh(z0, nil) -> nil
   filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
   if2(true, z0, z1, z2) -> filterhigh(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   append(nil, ys) -> ys
   append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   get(z0, nil) -> 0
   get(z0, cons(z1, nil)) -> z1
   get(0, cons(z0, cons(z1, z2))) -> z0
   get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

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

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

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


The TRS R consists of the following rules:

   QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
   QS(z0, nil) -> c1
   QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
   QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
   QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
   FILTERLOW(z0, nil) -> c7
   FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c11
   FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
   GE(z0, 0') -> c15
   GE(0', s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   APPEND(nil, ys) -> c18
   APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
   LENGTH(nil) -> c20
   LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
   HALF(0') -> c22
   HALF(s(0')) -> c23
   HALF(s(s(z0))) -> c24(HALF(z0))
   GET(z0, nil) -> c25
   GET(z0, cons(z1, nil)) -> c26
   GET(0', cons(z0, cons(z1, z2))) -> c27
   GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))

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

   qsort(z0) -> qs(half(length(z0)), z0)
   qs(z0, nil) -> nil
   qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
   filterlow(z0, nil) -> nil
   filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
   if1(true, z0, z1, z2) -> filterlow(z0, z2)
   if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
   filterhigh(z0, nil) -> nil
   filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
   if2(true, z0, z1, z2) -> filterhigh(z0, z2)
   if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   append(nil, ys) -> ys
   append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
   length(nil) -> 0'
   length(cons(z0, z1)) -> s(length(z1))
   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   get(z0, nil) -> 0'
   get(z0, cons(z1, nil)) -> z1
   get(0', cons(z0, cons(z1, z2))) -> z0
   get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
QS, half, length, HALF, LENGTH, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
half < QS
HALF < QS
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
half < qs
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(10)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
half, QS, length, HALF, LENGTH, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
half < QS
HALF < QS
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
half < qs
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)

Induction Base:
half(gen_0':s19_29(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s19_29(*(2, +(n24_29, 1)))) ->_R^Omega(0)
s(half(gen_0':s19_29(*(2, n24_29)))) ->_IH
s(gen_0':s19_29(c25_29))

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

(12)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
length, QS, HALF, LENGTH, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
HALF < QS
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)

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

Induction Step:
length(gen_nil:cons:ys15_29(+(n786_29, 1))) ->_R^Omega(0)
s(length(gen_nil:cons:ys15_29(n786_29))) ->_IH
s(gen_0':s19_29(c787_29))

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

(14)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
HALF, QS, LENGTH, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
HALF < QS
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s19_29(*(2, n1410_29))) -> gen_c22:c23:c2417_29(n1410_29), rt in Omega(1 + n1410_29)

Induction Base:
HALF(gen_0':s19_29(*(2, 0))) ->_R^Omega(1)
c22

Induction Step:
HALF(gen_0':s19_29(*(2, +(n1410_29, 1)))) ->_R^Omega(1)
c24(HALF(gen_0':s19_29(*(2, n1410_29)))) ->_IH
c24(gen_c22:c23:c2417_29(c1411_29))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
HALF, QS, LENGTH, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
HALF < QS
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)
HALF(gen_0':s19_29(*(2, n1410_29))) -> gen_c22:c23:c2417_29(n1410_29), rt in Omega(1 + n1410_29)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
LENGTH, QS, APPEND, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH(gen_nil:cons:ys15_29(n2085_29)) -> gen_c20:c2118_29(n2085_29), rt in Omega(1 + n2085_29)

Induction Base:
LENGTH(gen_nil:cons:ys15_29(0)) ->_R^Omega(1)
c20

Induction Step:
LENGTH(gen_nil:cons:ys15_29(+(n2085_29, 1))) ->_R^Omega(1)
c21(LENGTH(gen_nil:cons:ys15_29(n2085_29))) ->_IH
c21(gen_c20:c2118_29(c2086_29))

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

(22)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)
HALF(gen_0':s19_29(*(2, n1410_29))) -> gen_c22:c23:c2417_29(n1410_29), rt in Omega(1 + n1410_29)
LENGTH(gen_nil:cons:ys15_29(n2085_29)) -> gen_c20:c2118_29(n2085_29), rt in Omega(1 + n2085_29)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
APPEND, QS, qs, filterlow, get, filterhigh, FILTERLOW, GET, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
APPEND < QS
qs < QS
filterlow < QS
get < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
get < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
get(gen_0':s19_29(n2686_29), gen_nil:cons:ys15_29(+(1, n2686_29))) -> gen_0':s19_29(0), rt in Omega(0)

Induction Base:
get(gen_0':s19_29(0), gen_nil:cons:ys15_29(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
get(gen_0':s19_29(+(n2686_29, 1)), gen_nil:cons:ys15_29(+(1, +(n2686_29, 1)))) ->_R^Omega(0)
get(gen_0':s19_29(n2686_29), cons(0', gen_nil:cons:ys15_29(n2686_29))) ->_IH
gen_0':s19_29(0)

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

(24)
Obligation:
Innermost TRS:
Rules:
QSORT(z0) -> c(QS(half(length(z0)), z0), HALF(length(z0)), LENGTH(z0))
QS(z0, nil) -> c1
QS(z0, cons(z1, z2)) -> c2(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c3(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERLOW(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c4(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), GET(z0, cons(z1, z2)))
QS(z0, cons(z1, z2)) -> c5(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), HALF(z0))
QS(z0, cons(z1, z2)) -> c6(APPEND(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))))), QS(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2))), FILTERHIGH(get(z0, cons(z1, z2)), cons(z1, z2)), GET(z0, cons(z1, z2)))
FILTERLOW(z0, nil) -> c7
FILTERLOW(z0, cons(z1, z2)) -> c8(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c9(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c10(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c11
FILTERHIGH(z0, cons(z1, z2)) -> c12(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c13(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c14(FILTERHIGH(z0, z2))
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
APPEND(nil, ys) -> c18
APPEND(cons(z0, z1), ys) -> c19(APPEND(z1, ys))
LENGTH(nil) -> c20
LENGTH(cons(z0, z1)) -> c21(LENGTH(z1))
HALF(0') -> c22
HALF(s(0')) -> c23
HALF(s(s(z0))) -> c24(HALF(z0))
GET(z0, nil) -> c25
GET(z0, cons(z1, nil)) -> c26
GET(0', cons(z0, cons(z1, z2))) -> c27
GET(s(z0), cons(z1, cons(z2, z3))) -> c28(GET(z0, cons(z2, z3)))
qsort(z0) -> qs(half(length(z0)), z0)
qs(z0, nil) -> nil
qs(z0, cons(z1, z2)) -> append(qs(half(z0), filterlow(get(z0, cons(z1, z2)), cons(z1, z2))), cons(get(z0, cons(z1, z2)), qs(half(z0), filterhigh(get(z0, cons(z1, z2)), cons(z1, z2)))))
filterlow(z0, nil) -> nil
filterlow(z0, cons(z1, z2)) -> if1(ge(z0, z1), z0, z1, z2)
if1(true, z0, z1, z2) -> filterlow(z0, z2)
if1(false, z0, z1, z2) -> cons(z1, filterlow(z0, z2))
filterhigh(z0, nil) -> nil
filterhigh(z0, cons(z1, z2)) -> if2(ge(z1, z0), z0, z1, z2)
if2(true, z0, z1, z2) -> filterhigh(z0, z2)
if2(false, z0, z1, z2) -> cons(z1, filterhigh(z0, z2))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
append(nil, ys) -> ys
append(cons(z0, z1), ys) -> cons(z0, append(z1, ys))
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
get(z0, nil) -> 0'
get(z0, cons(z1, nil)) -> z1
get(0', cons(z0, cons(z1, z2))) -> z0
get(s(z0), cons(z1, cons(z2, z3))) -> get(z0, cons(z2, z3))

Types:
QSORT :: nil:cons:ys -> c
c :: c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c20:c21 -> c
QS :: 0':s -> nil:cons:ys -> c1:c2:c3:c4:c5:c6
half :: 0':s -> 0':s
length :: nil:cons:ys -> 0':s
HALF :: 0':s -> c22:c23:c24
LENGTH :: nil:cons:ys -> c20:c21
nil :: nil:cons:ys
c1 :: c1:c2:c3:c4:c5:c6
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c2 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
APPEND :: nil:cons:ys -> nil:cons:ys -> c18:c19
qs :: 0':s -> nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
get :: 0':s -> nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
c3 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c7:c8 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERLOW :: 0':s -> nil:cons:ys -> c7:c8
GET :: 0':s -> nil:cons:ys -> c25:c26:c27:c28
c4 :: c18:c19 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
c5 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c22:c23:c24 -> c1:c2:c3:c4:c5:c6
c6 :: c18:c19 -> c1:c2:c3:c4:c5:c6 -> c11:c12 -> c25:c26:c27:c28 -> c1:c2:c3:c4:c5:c6
FILTERHIGH :: 0':s -> nil:cons:ys -> c11:c12
c7 :: c7:c8
c8 :: c9:c10 -> c15:c16:c17 -> c7:c8
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c9:c10
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c15:c16:c17
true :: true:false
c9 :: c7:c8 -> c9:c10
false :: true:false
c10 :: c7:c8 -> c9:c10
c11 :: c11:c12
c12 :: c13:c14 -> c15:c16:c17 -> c11:c12
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c13:c14
c13 :: c11:c12 -> c13:c14
c14 :: c11:c12 -> c13:c14
0' :: 0':s
c15 :: c15:c16:c17
s :: 0':s -> 0':s
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
ys :: nil:cons:ys
c18 :: c18:c19
c19 :: c18:c19 -> c18:c19
c20 :: c20:c21
c21 :: c20:c21 -> c20:c21
c22 :: c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
c25 :: c25:c26:c27:c28
c26 :: c25:c26:c27:c28
c27 :: c25:c26:c27:c28
c28 :: c25:c26:c27:c28 -> c25:c26:c27:c28
qsort :: nil:cons:ys -> nil:cons:ys
append :: nil:cons:ys -> nil:cons:ys -> nil:cons:ys
if1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
if2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> nil:cons:ys
hole_c1_29 :: c
hole_nil:cons:ys2_29 :: nil:cons:ys
hole_c1:c2:c3:c4:c5:c63_29 :: c1:c2:c3:c4:c5:c6
hole_c22:c23:c244_29 :: c22:c23:c24
hole_c20:c215_29 :: c20:c21
hole_0':s6_29 :: 0':s
hole_c18:c197_29 :: c18:c19
hole_c7:c88_29 :: c7:c8
hole_c25:c26:c27:c289_29 :: c25:c26:c27:c28
hole_c11:c1210_29 :: c11:c12
hole_c9:c1011_29 :: c9:c10
hole_c15:c16:c1712_29 :: c15:c16:c17
hole_true:false13_29 :: true:false
hole_c13:c1414_29 :: c13:c14
gen_nil:cons:ys15_29 :: Nat -> nil:cons:ys
gen_c1:c2:c3:c4:c5:c616_29 :: Nat -> c1:c2:c3:c4:c5:c6
gen_c22:c23:c2417_29 :: Nat -> c22:c23:c24
gen_c20:c2118_29 :: Nat -> c20:c21
gen_0':s19_29 :: Nat -> 0':s
gen_c18:c1920_29 :: Nat -> c18:c19
gen_c25:c26:c27:c2821_29 :: Nat -> c25:c26:c27:c28
gen_c15:c16:c1722_29 :: Nat -> c15:c16:c17


Lemmas:
half(gen_0':s19_29(*(2, n24_29))) -> gen_0':s19_29(n24_29), rt in Omega(0)
length(gen_nil:cons:ys15_29(n786_29)) -> gen_0':s19_29(n786_29), rt in Omega(0)
HALF(gen_0':s19_29(*(2, n1410_29))) -> gen_c22:c23:c2417_29(n1410_29), rt in Omega(1 + n1410_29)
LENGTH(gen_nil:cons:ys15_29(n2085_29)) -> gen_c20:c2118_29(n2085_29), rt in Omega(1 + n2085_29)
get(gen_0':s19_29(n2686_29), gen_nil:cons:ys15_29(+(1, n2686_29))) -> gen_0':s19_29(0), rt in Omega(0)


Generator Equations:
gen_nil:cons:ys15_29(0) <=> nil
gen_nil:cons:ys15_29(+(x, 1)) <=> cons(0', gen_nil:cons:ys15_29(x))
gen_c1:c2:c3:c4:c5:c616_29(0) <=> c1
gen_c1:c2:c3:c4:c5:c616_29(+(x, 1)) <=> c2(c18, gen_c1:c2:c3:c4:c5:c616_29(x), c22)
gen_c22:c23:c2417_29(0) <=> c22
gen_c22:c23:c2417_29(+(x, 1)) <=> c24(gen_c22:c23:c2417_29(x))
gen_c20:c2118_29(0) <=> c20
gen_c20:c2118_29(+(x, 1)) <=> c21(gen_c20:c2118_29(x))
gen_0':s19_29(0) <=> 0'
gen_0':s19_29(+(x, 1)) <=> s(gen_0':s19_29(x))
gen_c18:c1920_29(0) <=> c18
gen_c18:c1920_29(+(x, 1)) <=> c19(gen_c18:c1920_29(x))
gen_c25:c26:c27:c2821_29(0) <=> c25
gen_c25:c26:c27:c2821_29(+(x, 1)) <=> c28(gen_c25:c26:c27:c2821_29(x))
gen_c15:c16:c1722_29(0) <=> c15
gen_c15:c16:c1722_29(+(x, 1)) <=> c17(gen_c15:c16:c1722_29(x))


The following defined symbols remain to be analysed:
GET, QS, qs, filterlow, filterhigh, FILTERLOW, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
qs < QS
filterlow < QS
filterhigh < QS
FILTERLOW < QS
GET < QS
FILTERHIGH < QS
filterlow < qs
filterhigh < qs
append < qs
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH