WORST_CASE(Omega(n^1),?)
proof of input_wrIeBdSp94.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), 0 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), 1 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 254 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 97.7 s]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 47 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 62 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 76 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 97 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 640 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 656 ms]
        (30) 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(nil) -> nil
   qsort(cons(x, xs)) -> append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(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))
   last(nil) -> 0
   last(cons(x, nil)) -> x
   last(cons(x, cons(y, xs))) -> last(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(nil) -> nil
   qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
   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))
   last(nil) -> 0
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
Tuples:
   QSORT(nil) -> c
   QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   FILTERLOW(z0, nil) -> c4
   FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c8
   FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c12
   GE(0, s(z0)) -> c13
   GE(s(z0), s(z1)) -> c14(GE(z0, z1))
   APPEND(nil, ys) -> c15
   APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
   LAST(nil) -> c17
   LAST(cons(z0, nil)) -> c18
   LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
S tuples:
   QSORT(nil) -> c
   QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   FILTERLOW(z0, nil) -> c4
   FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c8
   FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c12
   GE(0, s(z0)) -> c13
   GE(s(z0), s(z1)) -> c14(GE(z0, z1))
   APPEND(nil, ys) -> c15
   APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
   LAST(nil) -> c17
   LAST(cons(z0, nil)) -> c18
   LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
K tuples:none
Defined Rule Symbols:   qsort_1, filterlow_2, if1_4, filterhigh_2, if2_4, ge_2, append_2, last_1

Defined Pair Symbols:   QSORT_1, FILTERLOW_2, IF1_4, FILTERHIGH_2, IF2_4, GE_2, APPEND_2, LAST_1

Compound Symbols:   c, c1_4, c2_2, c3_4, c4, c5_2, c6_1, c7_1, c8, c9_2, c10_1, c11_1, c12, c13, c14_1, c15, c16_1, c17, c18, c19_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(nil) -> c
   QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   FILTERLOW(z0, nil) -> c4
   FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c8
   FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
   GE(z0, 0) -> c12
   GE(0, s(z0)) -> c13
   GE(s(z0), s(z1)) -> c14(GE(z0, z1))
   APPEND(nil, ys) -> c15
   APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
   LAST(nil) -> c17
   LAST(cons(z0, nil)) -> c18
   LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))

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

   qsort(nil) -> nil
   qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
   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))
   last(nil) -> 0
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

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(nil) -> c
   QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
   QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
   FILTERLOW(z0, nil) -> c4
   FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
   IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
   IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
   FILTERHIGH(z0, nil) -> c8
   FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
   IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
   IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
   GE(z0, 0') -> c12
   GE(0', s(z0)) -> c13
   GE(s(z0), s(z1)) -> c14(GE(z0, z1))
   APPEND(nil, ys) -> c15
   APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
   LAST(nil) -> c17
   LAST(cons(z0, nil)) -> c18
   LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))

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

   qsort(nil) -> nil
   qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
   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))
   last(nil) -> 0'
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
QSORT, APPEND, qsort, filterlow, last, filterhigh, FILTERLOW, LAST, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
qsort < QSORT
filterlow < QSORT
last < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
LAST < QSORT
FILTERHIGH < QSORT
filterlow < qsort
last < qsort
filterhigh < qsort
append < qsort
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(10)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
APPEND, QSORT, qsort, filterlow, last, filterhigh, FILTERLOW, LAST, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
qsort < QSORT
filterlow < QSORT
last < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
LAST < QSORT
FILTERHIGH < QSORT
filterlow < qsort
last < qsort
filterhigh < qsort
append < qsort
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)

Induction Base:
last(gen_nil:cons:ys13_20(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
last(gen_nil:cons:ys13_20(+(1, +(n29_20, 1)))) ->_R^Omega(0)
last(cons(0', gen_nil:cons:ys13_20(n29_20))) ->_IH
gen_0':s14_20(0)

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(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
LAST, QSORT, qsort, filterlow, filterhigh, FILTERLOW, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
qsort < QSORT
filterlow < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
LAST < QSORT
FILTERHIGH < QSORT
filterlow < qsort
filterhigh < qsort
append < qsort
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)

Induction Base:
LAST(gen_nil:cons:ys13_20(+(2, 0)))

Induction Step:
LAST(gen_nil:cons:ys13_20(+(2, +(n656_20, 1)))) ->_R^Omega(1)
c19(LAST(cons(0', gen_nil:cons:ys13_20(+(1, n656_20))))) ->_IH
c19(*18_20)

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
LAST, QSORT, qsort, filterlow, filterhigh, FILTERLOW, FILTERHIGH, ge, GE, append

They will be analysed ascendingly in the following order:
qsort < QSORT
filterlow < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
LAST < QSORT
FILTERHIGH < QSORT
filterlow < qsort
filterhigh < qsort
append < qsort
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
ge, QSORT, qsort, filterlow, filterhigh, FILTERLOW, FILTERHIGH, GE, append

They will be analysed ascendingly in the following order:
qsort < QSORT
filterlow < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
FILTERHIGH < QSORT
filterlow < qsort
filterhigh < qsort
append < qsort
ge < filterlow
ge < filterhigh
ge < FILTERLOW
GE < FILTERLOW
ge < FILTERHIGH
GE < FILTERHIGH

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s14_20(0), gen_0':s14_20(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s14_20(+(n74162_20, 1)), gen_0':s14_20(+(n74162_20, 1))) ->_R^Omega(0)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) ->_IH
true

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

(20)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
filterlow, QSORT, qsort, filterhigh, FILTERLOW, FILTERHIGH, GE, append

They will be analysed ascendingly in the following order:
qsort < QSORT
filterlow < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
FILTERHIGH < QSORT
filterlow < qsort
filterhigh < qsort
append < qsort
GE < FILTERLOW
GE < FILTERHIGH

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)

Induction Base:
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(0)) ->_R^Omega(0)
nil

Induction Step:
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(+(n74678_20, 1))) ->_R^Omega(0)
if1(ge(gen_0':s14_20(0), 0'), gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n74678_20)) ->_L^Omega(0)
if1(true, gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n74678_20)) ->_R^Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) ->_IH
gen_nil:cons:ys13_20(0)

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

(22)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
filterhigh, QSORT, qsort, FILTERLOW, FILTERHIGH, GE, append

They will be analysed ascendingly in the following order:
qsort < QSORT
filterhigh < QSORT
FILTERLOW < QSORT
FILTERHIGH < QSORT
filterhigh < qsort
append < qsort
GE < FILTERLOW
GE < FILTERHIGH

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)

Induction Base:
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(0)) ->_R^Omega(0)
nil

Induction Step:
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(+(n75940_20, 1))) ->_R^Omega(0)
if2(ge(0', gen_0':s14_20(0)), gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n75940_20)) ->_L^Omega(0)
if2(true, gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n75940_20)) ->_R^Omega(0)
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) ->_IH
gen_nil:cons:ys13_20(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(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
GE, QSORT, qsort, FILTERLOW, FILTERHIGH, append

They will be analysed ascendingly in the following order:
qsort < QSORT
FILTERLOW < QSORT
FILTERHIGH < QSORT
append < qsort
GE < FILTERLOW
GE < FILTERHIGH

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s14_20(n77221_20), gen_0':s14_20(n77221_20)) -> gen_c12:c13:c1417_20(n77221_20), rt in Omega(1 + n77221_20)

Induction Base:
GE(gen_0':s14_20(0), gen_0':s14_20(0)) ->_R^Omega(1)
c12

Induction Step:
GE(gen_0':s14_20(+(n77221_20, 1)), gen_0':s14_20(+(n77221_20, 1))) ->_R^Omega(1)
c14(GE(gen_0':s14_20(n77221_20), gen_0':s14_20(n77221_20))) ->_IH
c14(gen_c12:c13:c1417_20(c77222_20))

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

(26)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
GE(gen_0':s14_20(n77221_20), gen_0':s14_20(n77221_20)) -> gen_c12:c13:c1417_20(n77221_20), rt in Omega(1 + n77221_20)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
FILTERLOW, QSORT, qsort, FILTERHIGH, append

They will be analysed ascendingly in the following order:
qsort < QSORT
FILTERLOW < QSORT
FILTERHIGH < QSORT
append < qsort

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(n78243_20)) -> *18_20, rt in Omega(n78243_20)

Induction Base:
FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(0))

Induction Step:
FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(+(n78243_20, 1))) ->_R^Omega(1)
c5(IF1(ge(gen_0':s14_20(0), 0'), gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n78243_20)), GE(gen_0':s14_20(0), 0')) ->_L^Omega(0)
c5(IF1(true, gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n78243_20)), GE(gen_0':s14_20(0), 0')) ->_R^Omega(1)
c5(c6(FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(n78243_20))), GE(gen_0':s14_20(0), 0')) ->_IH
c5(c6(*18_20), GE(gen_0':s14_20(0), 0')) ->_L^Omega(1)
c5(c6(*18_20), gen_c12:c13:c1417_20(0))

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

(28)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
GE(gen_0':s14_20(n77221_20), gen_0':s14_20(n77221_20)) -> gen_c12:c13:c1417_20(n77221_20), rt in Omega(1 + n77221_20)
FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(n78243_20)) -> *18_20, rt in Omega(n78243_20)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
FILTERHIGH, QSORT, qsort, append

They will be analysed ascendingly in the following order:
qsort < QSORT
FILTERHIGH < QSORT
append < qsort

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FILTERHIGH(gen_0':s14_20(0), gen_nil:cons:ys13_20(n87469_20)) -> *18_20, rt in Omega(n87469_20)

Induction Base:
FILTERHIGH(gen_0':s14_20(0), gen_nil:cons:ys13_20(0))

Induction Step:
FILTERHIGH(gen_0':s14_20(0), gen_nil:cons:ys13_20(+(n87469_20, 1))) ->_R^Omega(1)
c9(IF2(ge(0', gen_0':s14_20(0)), gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n87469_20)), GE(0', gen_0':s14_20(0))) ->_L^Omega(0)
c9(IF2(true, gen_0':s14_20(0), 0', gen_nil:cons:ys13_20(n87469_20)), GE(0', gen_0':s14_20(0))) ->_R^Omega(1)
c9(c10(FILTERHIGH(gen_0':s14_20(0), gen_nil:cons:ys13_20(n87469_20))), GE(0', gen_0':s14_20(0))) ->_IH
c9(c10(*18_20), GE(0', gen_0':s14_20(0))) ->_L^Omega(1)
c9(c10(*18_20), gen_c12:c13:c1417_20(0))

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

(30)
Obligation:
Innermost TRS:
Rules:
QSORT(nil) -> c
QSORT(cons(z0, z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterlow(last(cons(z0, z1)), cons(z0, z1))), FILTERLOW(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), LAST(cons(z0, z1)))
QSORT(cons(z0, z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1))))), QSORT(filterhigh(last(cons(z0, z1)), cons(z0, z1))), FILTERHIGH(last(cons(z0, z1)), cons(z0, z1)), LAST(cons(z0, z1)))
FILTERLOW(z0, nil) -> c4
FILTERLOW(z0, cons(z1, z2)) -> c5(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1))
IF1(true, z0, z1, z2) -> c6(FILTERLOW(z0, z2))
IF1(false, z0, z1, z2) -> c7(FILTERLOW(z0, z2))
FILTERHIGH(z0, nil) -> c8
FILTERHIGH(z0, cons(z1, z2)) -> c9(IF2(ge(z1, z0), z0, z1, z2), GE(z1, z0))
IF2(true, z0, z1, z2) -> c10(FILTERHIGH(z0, z2))
IF2(false, z0, z1, z2) -> c11(FILTERHIGH(z0, z2))
GE(z0, 0') -> c12
GE(0', s(z0)) -> c13
GE(s(z0), s(z1)) -> c14(GE(z0, z1))
APPEND(nil, ys) -> c15
APPEND(cons(z0, z1), ys) -> c16(APPEND(z1, ys))
LAST(nil) -> c17
LAST(cons(z0, nil)) -> c18
LAST(cons(z0, cons(z1, z2))) -> c19(LAST(cons(z1, z2)))
qsort(nil) -> nil
qsort(cons(z0, z1)) -> append(qsort(filterlow(last(cons(z0, z1)), cons(z0, z1))), cons(last(cons(z0, z1)), qsort(filterhigh(last(cons(z0, z1)), cons(z0, z1)))))
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))
last(nil) -> 0'
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))

Types:
QSORT :: nil:cons:ys -> c:c1:c2:c3
nil :: nil:cons:ys
c :: c:c1:c2:c3
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c15:c16 -> c:c1:c2:c3 -> c4:c5 -> c17:c18:c19 -> c:c1:c2:c3
APPEND :: nil:cons:ys -> nil:cons:ys -> c15:c16
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
last :: nil:cons:ys -> 0':s
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c4:c5
LAST :: nil:cons:ys -> c17:c18:c19
c2 :: c15:c16 -> c17:c18:c19 -> c:c1:c2:c3
c3 :: c15:c16 -> c:c1:c2:c3 -> c8:c9 -> c17:c18:c19 -> c:c1:c2:c3
FILTERHIGH :: 0':s -> nil:cons:ys -> c8:c9
c4 :: c4:c5
c5 :: c6:c7 -> c12:c13:c14 -> c4:c5
IF1 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c6:c7
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c12:c13:c14
true :: true:false
c6 :: c4:c5 -> c6:c7
false :: true:false
c7 :: c4:c5 -> c6:c7
c8 :: c8:c9
c9 :: c10:c11 -> c12:c13:c14 -> c8:c9
IF2 :: true:false -> 0':s -> 0':s -> nil:cons:ys -> c10:c11
c10 :: c8:c9 -> c10:c11
c11 :: c8:c9 -> c10:c11
0' :: 0':s
c12 :: c12:c13:c14
s :: 0':s -> 0':s
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
ys :: nil:cons:ys
c15 :: c15:c16
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
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_c:c1:c2:c31_20 :: c:c1:c2:c3
hole_nil:cons:ys2_20 :: nil:cons:ys
hole_0':s3_20 :: 0':s
hole_c15:c164_20 :: c15:c16
hole_c4:c55_20 :: c4:c5
hole_c17:c18:c196_20 :: c17:c18:c19
hole_c8:c97_20 :: c8:c9
hole_c6:c78_20 :: c6:c7
hole_c12:c13:c149_20 :: c12:c13:c14
hole_true:false10_20 :: true:false
hole_c10:c1111_20 :: c10:c11
gen_c:c1:c2:c312_20 :: Nat -> c:c1:c2:c3
gen_nil:cons:ys13_20 :: Nat -> nil:cons:ys
gen_0':s14_20 :: Nat -> 0':s
gen_c15:c1615_20 :: Nat -> c15:c16
gen_c17:c18:c1916_20 :: Nat -> c17:c18:c19
gen_c12:c13:c1417_20 :: Nat -> c12:c13:c14


Lemmas:
last(gen_nil:cons:ys13_20(+(1, n29_20))) -> gen_0':s14_20(0), rt in Omega(0)
LAST(gen_nil:cons:ys13_20(+(2, n656_20))) -> *18_20, rt in Omega(n656_20)
ge(gen_0':s14_20(n74162_20), gen_0':s14_20(n74162_20)) -> true, rt in Omega(0)
filterlow(gen_0':s14_20(0), gen_nil:cons:ys13_20(n74678_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
filterhigh(gen_0':s14_20(0), gen_nil:cons:ys13_20(n75940_20)) -> gen_nil:cons:ys13_20(0), rt in Omega(0)
GE(gen_0':s14_20(n77221_20), gen_0':s14_20(n77221_20)) -> gen_c12:c13:c1417_20(n77221_20), rt in Omega(1 + n77221_20)
FILTERLOW(gen_0':s14_20(0), gen_nil:cons:ys13_20(n78243_20)) -> *18_20, rt in Omega(n78243_20)
FILTERHIGH(gen_0':s14_20(0), gen_nil:cons:ys13_20(n87469_20)) -> *18_20, rt in Omega(n87469_20)


Generator Equations:
gen_c:c1:c2:c312_20(0) <=> c
gen_c:c1:c2:c312_20(+(x, 1)) <=> c1(c15, gen_c:c1:c2:c312_20(x), c4, c17)
gen_nil:cons:ys13_20(0) <=> nil
gen_nil:cons:ys13_20(+(x, 1)) <=> cons(0', gen_nil:cons:ys13_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c15:c1615_20(0) <=> c15
gen_c15:c1615_20(+(x, 1)) <=> c16(gen_c15:c1615_20(x))
gen_c17:c18:c1916_20(0) <=> c17
gen_c17:c18:c1916_20(+(x, 1)) <=> c19(gen_c17:c18:c1916_20(x))
gen_c12:c13:c1417_20(0) <=> c12
gen_c12:c13:c1417_20(+(x, 1)) <=> c14(gen_c12:c13:c1417_20(x))


The following defined symbols remain to be analysed:
append, QSORT, qsort

They will be analysed ascendingly in the following order:
qsort < QSORT
append < qsort