WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 6144 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 7 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 260 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 26 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 13 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 104 ms]
(18) BEST
    (19) proven lower bound
        (20) LowerBoundPropagationProof [FINISHED, 0 ms]
        (21) BOUNDS(n^1, INF)
    (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 656 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 672 ms]
        (26) typed CpxTrs


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF1/2
IF2/2

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

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

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

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

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

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13

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

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

They will be analysed ascendingly in the following order:
APPEND < QSORT
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

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(x))


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

They will be analysed ascendingly in the following order:
APPEND < QSORT
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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)

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

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)

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

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)

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

Induction Step:
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(+(n1384_16, 1))) ->_R^Omega(0)
if2(ge(0', gen_0':s13_16(0)), gen_0':s13_16(0), 0', gen_nil:cons:ys12_16(n1384_16)) ->_L^Omega(0)
if2(true, gen_0':s13_16(0), 0', gen_nil:cons:ys12_16(n1384_16)) ->_R^Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) ->_IH
gen_nil:cons:ys12_16(0)

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s13_16(n2372_16), gen_0':s13_16(n2372_16)) -> gen_c11:c12:c1315_16(n2372_16), rt in Omega(1 + n2372_16)

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

Induction Step:
GE(gen_0':s13_16(+(n2372_16, 1)), gen_0':s13_16(+(n2372_16, 1))) ->_R^Omega(1)
c13(GE(gen_0':s13_16(n2372_16), gen_0':s13_16(n2372_16))) ->_IH
c13(gen_c11:c12:c1315_16(c2373_16))

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

(18)
Complex Obligation (BEST)

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

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

(21)
BOUNDS(n^1, INF)

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
GE(gen_0':s13_16(n2372_16), gen_0':s13_16(n2372_16)) -> gen_c11:c12:c1315_16(n2372_16), rt in Omega(1 + n2372_16)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16)) -> *16_16, rt in Omega(n3161_16)

Induction Base:
FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(0))

Induction Step:
FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(+(n3161_16, 1))) ->_R^Omega(1)
c4(IF1(ge(gen_0':s13_16(0), 0'), gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16)), GE(gen_0':s13_16(0), 0')) ->_L^Omega(0)
c4(IF1(true, gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16)), GE(gen_0':s13_16(0), 0')) ->_R^Omega(1)
c4(c5(FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16))), GE(gen_0':s13_16(0), 0')) ->_IH
c4(c5(*16_16), GE(gen_0':s13_16(0), 0')) ->_L^Omega(1)
c4(c5(*16_16), gen_c11:c12:c1315_16(0))

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

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
GE(gen_0':s13_16(n2372_16), gen_0':s13_16(n2372_16)) -> gen_c11:c12:c1315_16(n2372_16), rt in Omega(1 + n2372_16)
FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16)) -> *16_16, rt in Omega(n3161_16)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FILTERHIGH(gen_0':s13_16(0), gen_nil:cons:ys12_16(n8191_16)) -> *16_16, rt in Omega(n8191_16)

Induction Base:
FILTERHIGH(gen_0':s13_16(0), gen_nil:cons:ys12_16(0))

Induction Step:
FILTERHIGH(gen_0':s13_16(0), gen_nil:cons:ys12_16(+(n8191_16, 1))) ->_R^Omega(1)
c8(IF2(ge(0', gen_0':s13_16(0)), gen_0':s13_16(0), gen_nil:cons:ys12_16(n8191_16)), GE(0', gen_0':s13_16(0))) ->_L^Omega(0)
c8(IF2(true, gen_0':s13_16(0), gen_nil:cons:ys12_16(n8191_16)), GE(0', gen_0':s13_16(0))) ->_R^Omega(1)
c8(c9(FILTERHIGH(gen_0':s13_16(0), gen_nil:cons:ys12_16(n8191_16))), GE(0', gen_0':s13_16(0))) ->_IH
c8(c9(*16_16), GE(0', gen_0':s13_16(0))) ->_L^Omega(1)
c8(c9(*16_16), gen_c11:c12:c1315_16(0))

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

Types:
QSORT :: nil:cons:ys -> c:c1:c2
nil :: nil:cons:ys
c :: c:c1:c2
cons :: 0':s -> nil:cons:ys -> nil:cons:ys
c1 :: c14:c15 -> c:c1:c2 -> c3:c4 -> c:c1:c2
APPEND :: nil:cons:ys -> nil:cons:ys -> c14:c15
qsort :: nil:cons:ys -> nil:cons:ys
filterlow :: 0':s -> nil:cons:ys -> nil:cons:ys
filterhigh :: 0':s -> nil:cons:ys -> nil:cons:ys
FILTERLOW :: 0':s -> nil:cons:ys -> c3:c4
c2 :: c14:c15 -> c:c1:c2 -> c7:c8 -> c:c1:c2
FILTERHIGH :: 0':s -> nil:cons:ys -> c7:c8
c3 :: c3:c4
c4 :: c5:c6 -> c11:c12:c13 -> c3:c4
IF1 :: true:false -> 0':s -> nil:cons:ys -> c5:c6
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c11:c12:c13
true :: true:false
c5 :: c3:c4 -> c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c11:c12:c13 -> c7:c8
IF2 :: true:false -> 0':s -> nil:cons:ys -> c9:c10
c9 :: c7:c8 -> c9:c10
c10 :: c7:c8 -> c9:c10
0' :: 0':s
c11 :: c11:c12:c13
s :: 0':s -> 0':s
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
ys :: nil:cons:ys
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
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:c21_16 :: c:c1:c2
hole_nil:cons:ys2_16 :: nil:cons:ys
hole_0':s3_16 :: 0':s
hole_c14:c154_16 :: c14:c15
hole_c3:c45_16 :: c3:c4
hole_c7:c86_16 :: c7:c8
hole_c5:c67_16 :: c5:c6
hole_c11:c12:c138_16 :: c11:c12:c13
hole_true:false9_16 :: true:false
hole_c9:c1010_16 :: c9:c10
gen_c:c1:c211_16 :: Nat -> c:c1:c2
gen_nil:cons:ys12_16 :: Nat -> nil:cons:ys
gen_0':s13_16 :: Nat -> 0':s
gen_c14:c1514_16 :: Nat -> c14:c15
gen_c11:c12:c1315_16 :: Nat -> c11:c12:c13


Lemmas:
ge(gen_0':s13_16(n27_16), gen_0':s13_16(n27_16)) -> true, rt in Omega(0)
filterlow(gen_0':s13_16(0), gen_nil:cons:ys12_16(n415_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
filterhigh(gen_0':s13_16(0), gen_nil:cons:ys12_16(n1384_16)) -> gen_nil:cons:ys12_16(0), rt in Omega(0)
GE(gen_0':s13_16(n2372_16), gen_0':s13_16(n2372_16)) -> gen_c11:c12:c1315_16(n2372_16), rt in Omega(1 + n2372_16)
FILTERLOW(gen_0':s13_16(0), gen_nil:cons:ys12_16(n3161_16)) -> *16_16, rt in Omega(n3161_16)
FILTERHIGH(gen_0':s13_16(0), gen_nil:cons:ys12_16(n8191_16)) -> *16_16, rt in Omega(n8191_16)


Generator Equations:
gen_c:c1:c211_16(0) <=> c
gen_c:c1:c211_16(+(x, 1)) <=> c1(c14, gen_c:c1:c211_16(x), c3)
gen_nil:cons:ys12_16(0) <=> nil
gen_nil:cons:ys12_16(+(x, 1)) <=> cons(0', gen_nil:cons:ys12_16(x))
gen_0':s13_16(0) <=> 0'
gen_0':s13_16(+(x, 1)) <=> s(gen_0':s13_16(x))
gen_c14:c1514_16(0) <=> c14
gen_c14:c1514_16(+(x, 1)) <=> c15(gen_c14:c1514_16(x))
gen_c11:c12:c1315_16(0) <=> c11
gen_c11:c12:c1315_16(+(x, 1)) <=> c13(gen_c11:c12:c1315_16(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