WORST_CASE(Omega(n^2),?)
proof of input_bKyyp10MRt.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, 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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 366 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 29 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 9 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 686 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 602 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 70 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 68 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 86 ms]
        (30) typed CpxTrs
        (31) RewriteLemmaProof [LOWER BOUND(ID), 457 ms]
        (32) typed CpxTrs
        (33) RewriteLemmaProof [LOWER BOUND(ID), 40.1 s]
        (34) proven lower bound
        (35) LowerBoundPropagationProof [FINISHED, 0 ms]
        (36) BOUNDS(n^2, INF)


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

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


The TRS R consists of the following rules:

   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   app(nil, y) -> y
   app(add(n, x), y) -> add(n, app(x, y))
   low(n, nil) -> nil
   low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
   if_low(true, n, add(m, x)) -> add(m, low(n, x))
   if_low(false, n, add(m, x)) -> low(n, x)
   high(n, nil) -> nil
   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
   if_high(true, n, add(m, x)) -> high(n, x)
   if_high(false, n, add(m, x)) -> add(m, high(n, x))
   head(add(n, x)) -> n
   tail(add(n, x)) -> x
   isempty(nil) -> true
   isempty(add(n, x)) -> false
   quicksort(x) -> if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
   if_qs(true, x, n, y) -> nil
   if_qs(false, x, n, y) -> app(quicksort(x), add(n, quicksort(y)))

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:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   low(z0, nil) -> nil
   low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
   if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
   if_low(false, z0, add(z1, z2)) -> low(z0, z2)
   high(z0, nil) -> nil
   high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
   if_high(true, z0, add(z1, z2)) -> high(z0, z2)
   if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   isempty(nil) -> true
   isempty(add(z0, z1)) -> false
   quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
   if_qs(true, z0, z1, z2) -> nil
   if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   APP(nil, z0) -> c3
   APP(add(z0, z1), z2) -> c4(APP(z1, z2))
   LOW(z0, nil) -> c5
   LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
   HIGH(z0, nil) -> c9
   HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   ISEMPTY(nil) -> c15
   ISEMPTY(add(z0, z1)) -> c16
   QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
   QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
   QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
   QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
   IF_QS(true, z0, z1, z2) -> c23
   IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
   IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   APP(nil, z0) -> c3
   APP(add(z0, z1), z2) -> c4(APP(z1, z2))
   LOW(z0, nil) -> c5
   LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
   HIGH(z0, nil) -> c9
   HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   ISEMPTY(nil) -> c15
   ISEMPTY(add(z0, z1)) -> c16
   QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
   QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
   QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
   QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
   IF_QS(true, z0, z1, z2) -> c23
   IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
   IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
K tuples:none
Defined Rule Symbols:   le_2, app_2, low_2, if_low_3, high_2, if_high_3, head_1, tail_1, isempty_1, quicksort_1, if_qs_4

Defined Pair Symbols:   LE_2, APP_2, LOW_2, IF_LOW_3, HIGH_2, IF_HIGH_3, HEAD_1, TAIL_1, ISEMPTY_1, QUICKSORT_1, IF_QS_4

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5, c6_2, c7_1, c8_1, c9, c10_2, c11_1, c12_1, c13, c14, c15, c16, c17_2, c18_3, c19_3, c20_2, c21_3, c22_3, c23, c24_2, c25_2


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

(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^2, INF).


The TRS R consists of the following rules:

   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   APP(nil, z0) -> c3
   APP(add(z0, z1), z2) -> c4(APP(z1, z2))
   LOW(z0, nil) -> c5
   LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
   HIGH(z0, nil) -> c9
   HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   ISEMPTY(nil) -> c15
   ISEMPTY(add(z0, z1)) -> c16
   QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
   QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
   QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
   QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
   IF_QS(true, z0, z1, z2) -> c23
   IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
   IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   low(z0, nil) -> nil
   low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
   if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
   if_low(false, z0, add(z1, z2)) -> low(z0, z2)
   high(z0, nil) -> nil
   high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
   if_high(true, z0, add(z1, z2)) -> high(z0, z2)
   if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   isempty(nil) -> true
   isempty(add(z0, z1)) -> false
   quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
   if_qs(true, z0, z1, z2) -> nil
   if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(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^2, INF).


The TRS R consists of the following rules:

   LE(0', z0) -> c
   LE(s(z0), 0') -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   APP(nil, z0) -> c3
   APP(add(z0, z1), z2) -> c4(APP(z1, z2))
   LOW(z0, nil) -> c5
   LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
   HIGH(z0, nil) -> c9
   HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
   HEAD(add(z0, z1)) -> c13
   TAIL(add(z0, z1)) -> c14
   ISEMPTY(nil) -> c15
   ISEMPTY(add(z0, z1)) -> c16
   QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
   QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
   QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
   QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
   QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
   IF_QS(true, z0, z1, z2) -> c23
   IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
   IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))

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

   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   app(nil, z0) -> z0
   app(add(z0, z1), z2) -> add(z0, app(z1, z2))
   low(z0, nil) -> nil
   low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
   if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
   if_low(false, z0, add(z1, z2)) -> low(z0, z2)
   high(z0, nil) -> nil
   high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
   if_high(true, z0, add(z1, z2)) -> high(z0, z2)
   if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
   head(add(z0, z1)) -> z0
   tail(add(z0, z1)) -> z1
   isempty(nil) -> true
   isempty(add(z0, z1)) -> false
   quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
   if_qs(true, z0, z1, z2) -> nil
   if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, APP, LOW, le, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
LE < LOW
LE < HIGH
APP < QUICKSORT
le < LOW
LOW < QUICKSORT
le < HIGH
le < low
le < high
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(10)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
LE, APP, LOW, le, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
LE < LOW
LE < HIGH
APP < QUICKSORT
le < LOW
LOW < QUICKSORT
le < HIGH
le < low
le < high
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)

Induction Base:
LE(gen_0':s16_26(0), gen_0':s16_26(0)) ->_R^Omega(1)
c

Induction Step:
LE(gen_0':s16_26(+(n20_26, 1)), gen_0':s16_26(+(n20_26, 1))) ->_R^Omega(1)
c2(LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26))) ->_IH
c2(gen_c:c1:c215_26(c21_26))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
LE, APP, LOW, le, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
LE < LOW
LE < HIGH
APP < QUICKSORT
le < LOW
LOW < QUICKSORT
le < HIGH
le < low
le < high
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
APP, LOW, le, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
APP < QUICKSORT
le < LOW
LOW < QUICKSORT
le < HIGH
le < low
le < high
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)

Induction Base:
APP(gen_nil:add18_26(0), gen_nil:add18_26(b)) ->_R^Omega(1)
c3

Induction Step:
APP(gen_nil:add18_26(+(n754_26, 1)), gen_nil:add18_26(b)) ->_R^Omega(1)
c4(APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b))) ->_IH
c4(gen_c3:c417_26(c755_26))

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

(18)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
le, LOW, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
le < LOW
LOW < QUICKSORT
le < HIGH
le < low
le < high
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s16_26(0), gen_0':s16_26(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s16_26(+(n1772_26, 1)), gen_0':s16_26(+(n1772_26, 1))) ->_R^Omega(0)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) ->_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:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
LOW, HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
LOW < QUICKSORT
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)

Induction Base:
LOW(gen_0':s16_26(0), gen_nil:add18_26(0))

Induction Step:
LOW(gen_0':s16_26(0), gen_nil:add18_26(+(n2265_26, 1))) ->_R^Omega(1)
c6(IF_LOW(le(0', gen_0':s16_26(0)), gen_0':s16_26(0), add(0', gen_nil:add18_26(n2265_26))), LE(0', gen_0':s16_26(0))) ->_L^Omega(0)
c6(IF_LOW(true, gen_0':s16_26(0), add(0', gen_nil:add18_26(n2265_26))), LE(0', gen_0':s16_26(0))) ->_R^Omega(1)
c6(c7(LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26))), LE(0', gen_0':s16_26(0))) ->_IH
c6(c7(*19_26), LE(0', gen_0':s16_26(0))) ->_L^Omega(1)
c6(c7(*19_26), gen_c:c1:c215_26(0))

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

(22)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
HIGH, QUICKSORT, low, high, quicksort, app

They will be analysed ascendingly in the following order:
HIGH < QUICKSORT
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)

Induction Base:
HIGH(gen_0':s16_26(0), gen_nil:add18_26(0))

Induction Step:
HIGH(gen_0':s16_26(0), gen_nil:add18_26(+(n7047_26, 1))) ->_R^Omega(1)
c10(IF_HIGH(le(0', gen_0':s16_26(0)), gen_0':s16_26(0), add(0', gen_nil:add18_26(n7047_26))), LE(0', gen_0':s16_26(0))) ->_L^Omega(0)
c10(IF_HIGH(true, gen_0':s16_26(0), add(0', gen_nil:add18_26(n7047_26))), LE(0', gen_0':s16_26(0))) ->_R^Omega(1)
c10(c11(HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26))), LE(0', gen_0':s16_26(0))) ->_IH
c10(c11(*19_26), LE(0', gen_0':s16_26(0))) ->_L^Omega(1)
c10(c11(*19_26), gen_c:c1:c215_26(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:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
low, QUICKSORT, high, quicksort, app

They will be analysed ascendingly in the following order:
low < QUICKSORT
high < QUICKSORT
quicksort < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)

Induction Base:
low(gen_0':s16_26(0), gen_nil:add18_26(0)) ->_R^Omega(0)
nil

Induction Step:
low(gen_0':s16_26(0), gen_nil:add18_26(+(n14737_26, 1))) ->_R^Omega(0)
if_low(le(0', gen_0':s16_26(0)), gen_0':s16_26(0), add(0', gen_nil:add18_26(n14737_26))) ->_L^Omega(0)
if_low(true, gen_0':s16_26(0), add(0', gen_nil:add18_26(n14737_26))) ->_R^Omega(0)
add(0', low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26))) ->_IH
add(0', gen_nil:add18_26(c14738_26))

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

(26)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
high, QUICKSORT, quicksort, app

They will be analysed ascendingly in the following order:
high < QUICKSORT
quicksort < QUICKSORT
high < quicksort
app < quicksort

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) -> gen_nil:add18_26(0), rt in Omega(0)

Induction Base:
high(gen_0':s16_26(0), gen_nil:add18_26(0)) ->_R^Omega(0)
nil

Induction Step:
high(gen_0':s16_26(0), gen_nil:add18_26(+(n16288_26, 1))) ->_R^Omega(0)
if_high(le(0', gen_0':s16_26(0)), gen_0':s16_26(0), add(0', gen_nil:add18_26(n16288_26))) ->_L^Omega(0)
if_high(true, gen_0':s16_26(0), add(0', gen_nil:add18_26(n16288_26))) ->_R^Omega(0)
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) ->_IH
gen_nil:add18_26(0)

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

(28)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) -> gen_nil:add18_26(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
app, QUICKSORT, quicksort

They will be analysed ascendingly in the following order:
quicksort < QUICKSORT
app < quicksort

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
app(gen_nil:add18_26(n17743_26), gen_nil:add18_26(b)) -> gen_nil:add18_26(+(n17743_26, b)), rt in Omega(0)

Induction Base:
app(gen_nil:add18_26(0), gen_nil:add18_26(b)) ->_R^Omega(0)
gen_nil:add18_26(b)

Induction Step:
app(gen_nil:add18_26(+(n17743_26, 1)), gen_nil:add18_26(b)) ->_R^Omega(0)
add(0', app(gen_nil:add18_26(n17743_26), gen_nil:add18_26(b))) ->_IH
add(0', gen_nil:add18_26(+(b, c17744_26)))

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

(30)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) -> gen_nil:add18_26(0), rt in Omega(0)
app(gen_nil:add18_26(n17743_26), gen_nil:add18_26(b)) -> gen_nil:add18_26(+(n17743_26, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
quicksort, QUICKSORT

They will be analysed ascendingly in the following order:
quicksort < QUICKSORT

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
quicksort(gen_nil:add18_26(n20042_26)) -> gen_nil:add18_26(n20042_26), rt in Omega(0)

Induction Base:
quicksort(gen_nil:add18_26(0)) ->_R^Omega(0)
if_qs(isempty(gen_nil:add18_26(0)), low(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0))), head(gen_nil:add18_26(0)), high(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0)))) ->_R^Omega(0)
if_qs(true, low(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0))), head(gen_nil:add18_26(0)), high(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0)))) ->_R^Omega(0)
nil

Induction Step:
quicksort(gen_nil:add18_26(+(n20042_26, 1))) ->_R^Omega(0)
if_qs(isempty(gen_nil:add18_26(+(n20042_26, 1))), low(head(gen_nil:add18_26(+(n20042_26, 1))), tail(gen_nil:add18_26(+(n20042_26, 1)))), head(gen_nil:add18_26(+(n20042_26, 1))), high(head(gen_nil:add18_26(+(n20042_26, 1))), tail(gen_nil:add18_26(+(n20042_26, 1))))) ->_R^Omega(0)
if_qs(false, low(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26)))), head(gen_nil:add18_26(+(1, n20042_26))), high(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26))))) ->_R^Omega(0)
if_qs(false, low(0', tail(gen_nil:add18_26(+(1, n20042_26)))), head(gen_nil:add18_26(+(1, n20042_26))), high(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26))))) ->_R^Omega(0)
if_qs(false, low(0', gen_nil:add18_26(n20042_26)), head(gen_nil:add18_26(+(1, n20042_26))), high(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26))))) ->_L^Omega(0)
if_qs(false, gen_nil:add18_26(n20042_26), head(gen_nil:add18_26(+(1, n20042_26))), high(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26))))) ->_R^Omega(0)
if_qs(false, gen_nil:add18_26(n20042_26), 0', high(head(gen_nil:add18_26(+(1, n20042_26))), tail(gen_nil:add18_26(+(1, n20042_26))))) ->_R^Omega(0)
if_qs(false, gen_nil:add18_26(n20042_26), 0', high(0', tail(gen_nil:add18_26(+(1, n20042_26))))) ->_R^Omega(0)
if_qs(false, gen_nil:add18_26(n20042_26), 0', high(0', gen_nil:add18_26(n20042_26))) ->_L^Omega(0)
if_qs(false, gen_nil:add18_26(n20042_26), 0', gen_nil:add18_26(0)) ->_R^Omega(0)
app(quicksort(gen_nil:add18_26(n20042_26)), add(0', quicksort(gen_nil:add18_26(0)))) ->_IH
app(gen_nil:add18_26(c20043_26), add(0', quicksort(gen_nil:add18_26(0)))) ->_R^Omega(0)
app(gen_nil:add18_26(n20042_26), add(0', if_qs(isempty(gen_nil:add18_26(0)), low(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0))), head(gen_nil:add18_26(0)), high(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0)))))) ->_R^Omega(0)
app(gen_nil:add18_26(n20042_26), add(0', if_qs(true, low(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0))), head(gen_nil:add18_26(0)), high(head(gen_nil:add18_26(0)), tail(gen_nil:add18_26(0)))))) ->_R^Omega(0)
app(gen_nil:add18_26(n20042_26), add(0', nil)) ->_L^Omega(0)
gen_nil:add18_26(+(n20042_26, +(0, 1)))

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

(32)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) -> gen_nil:add18_26(0), rt in Omega(0)
app(gen_nil:add18_26(n17743_26), gen_nil:add18_26(b)) -> gen_nil:add18_26(+(n17743_26, b)), rt in Omega(0)
quicksort(gen_nil:add18_26(n20042_26)) -> gen_nil:add18_26(n20042_26), rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
QUICKSORT
----------------------------------------

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
QUICKSORT(gen_nil:add18_26(n27118_26)) -> *19_26, rt in Omega(n27118_26 + n27118_26^2)

Induction Base:
QUICKSORT(gen_nil:add18_26(0))

Induction Step:
QUICKSORT(gen_nil:add18_26(+(n27118_26, 1))) ->_R^Omega(1)
c17(IF_QS(isempty(gen_nil:add18_26(+(n27118_26, 1))), low(head(gen_nil:add18_26(+(n27118_26, 1))), tail(gen_nil:add18_26(+(n27118_26, 1)))), head(gen_nil:add18_26(+(n27118_26, 1))), high(head(gen_nil:add18_26(+(n27118_26, 1))), tail(gen_nil:add18_26(+(n27118_26, 1))))), ISEMPTY(gen_nil:add18_26(+(n27118_26, 1)))) ->_R^Omega(0)
c17(IF_QS(false, low(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26)))), head(gen_nil:add18_26(+(1, n27118_26))), high(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(0)
c17(IF_QS(false, low(0', tail(gen_nil:add18_26(+(1, n27118_26)))), head(gen_nil:add18_26(+(1, n27118_26))), high(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(0)
c17(IF_QS(false, low(0', gen_nil:add18_26(n27118_26)), head(gen_nil:add18_26(+(1, n27118_26))), high(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_L^Omega(0)
c17(IF_QS(false, gen_nil:add18_26(n27118_26), head(gen_nil:add18_26(+(1, n27118_26))), high(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(0)
c17(IF_QS(false, gen_nil:add18_26(n27118_26), 0', high(head(gen_nil:add18_26(+(1, n27118_26))), tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(0)
c17(IF_QS(false, gen_nil:add18_26(n27118_26), 0', high(0', tail(gen_nil:add18_26(+(1, n27118_26))))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(0)
c17(IF_QS(false, gen_nil:add18_26(n27118_26), 0', high(0', gen_nil:add18_26(n27118_26))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_L^Omega(0)
c17(IF_QS(false, gen_nil:add18_26(n27118_26), 0', gen_nil:add18_26(0)), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(1)
c17(c24(APP(quicksort(gen_nil:add18_26(n27118_26)), add(0', quicksort(gen_nil:add18_26(0)))), QUICKSORT(gen_nil:add18_26(n27118_26))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_L^Omega(0)
c17(c24(APP(gen_nil:add18_26(n27118_26), add(0', quicksort(gen_nil:add18_26(0)))), QUICKSORT(gen_nil:add18_26(n27118_26))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_L^Omega(0)
c17(c24(APP(gen_nil:add18_26(n27118_26), add(0', gen_nil:add18_26(0))), QUICKSORT(gen_nil:add18_26(n27118_26))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_L^Omega(1 + n27118_26)
c17(c24(gen_c3:c417_26(n27118_26), QUICKSORT(gen_nil:add18_26(n27118_26))), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_IH
c17(c24(gen_c3:c417_26(n27118_26), *19_26), ISEMPTY(gen_nil:add18_26(+(1, n27118_26)))) ->_R^Omega(1)
c17(c24(gen_c3:c417_26(n27118_26), *19_26), c16)

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

(34)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
APP(nil, z0) -> c3
APP(add(z0, z1), z2) -> c4(APP(z1, z2))
LOW(z0, nil) -> c5
LOW(z0, add(z1, z2)) -> c6(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c7(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c8(LOW(z0, z2))
HIGH(z0, nil) -> c9
HIGH(z0, add(z1, z2)) -> c10(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c11(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c12(HIGH(z0, z2))
HEAD(add(z0, z1)) -> c13
TAIL(add(z0, z1)) -> c14
ISEMPTY(nil) -> c15
ISEMPTY(add(z0, z1)) -> c16
QUICKSORT(z0) -> c17(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), ISEMPTY(z0))
QUICKSORT(z0) -> c18(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c19(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), LOW(head(z0), tail(z0)), TAIL(z0))
QUICKSORT(z0) -> c20(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HEAD(z0))
QUICKSORT(z0) -> c21(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), HEAD(z0))
QUICKSORT(z0) -> c22(IF_QS(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0))), HIGH(head(z0), tail(z0)), TAIL(z0))
IF_QS(true, z0, z1, z2) -> c23
IF_QS(false, z0, z1, z2) -> c24(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z0))
IF_QS(false, z0, z1, z2) -> c25(APP(quicksort(z0), add(z1, quicksort(z2))), QUICKSORT(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
app(nil, z0) -> z0
app(add(z0, z1), z2) -> add(z0, app(z1, z2))
low(z0, nil) -> nil
low(z0, add(z1, z2)) -> if_low(le(z1, z0), z0, add(z1, z2))
if_low(true, z0, add(z1, z2)) -> add(z1, low(z0, z2))
if_low(false, z0, add(z1, z2)) -> low(z0, z2)
high(z0, nil) -> nil
high(z0, add(z1, z2)) -> if_high(le(z1, z0), z0, add(z1, z2))
if_high(true, z0, add(z1, z2)) -> high(z0, z2)
if_high(false, z0, add(z1, z2)) -> add(z1, high(z0, z2))
head(add(z0, z1)) -> z0
tail(add(z0, z1)) -> z1
isempty(nil) -> true
isempty(add(z0, z1)) -> false
quicksort(z0) -> if_qs(isempty(z0), low(head(z0), tail(z0)), head(z0), high(head(z0), tail(z0)))
if_qs(true, z0, z1, z2) -> nil
if_qs(false, z0, z1, z2) -> app(quicksort(z0), add(z1, quicksort(z2)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APP :: nil:add -> nil:add -> c3:c4
nil :: nil:add
c3 :: c3:c4
add :: 0':s -> nil:add -> nil:add
c4 :: c3:c4 -> c3:c4
LOW :: 0':s -> nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c:c1:c2 -> c5:c6
IF_LOW :: true:false -> 0':s -> nil:add -> c7:c8
le :: 0':s -> 0':s -> true:false
true :: true:false
c7 :: c5:c6 -> c7:c8
false :: true:false
c8 :: c5:c6 -> c7:c8
HIGH :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c:c1:c2 -> c9:c10
IF_HIGH :: true:false -> 0':s -> nil:add -> c11:c12
c11 :: c9:c10 -> c11:c12
c12 :: c9:c10 -> c11:c12
HEAD :: nil:add -> c13
c13 :: c13
TAIL :: nil:add -> c14
c14 :: c14
ISEMPTY :: nil:add -> c15:c16
c15 :: c15:c16
c16 :: c15:c16
QUICKSORT :: nil:add -> c17:c18:c19:c20:c21:c22
c17 :: c23:c24:c25 -> c15:c16 -> c17:c18:c19:c20:c21:c22
IF_QS :: true:false -> nil:add -> 0':s -> nil:add -> c23:c24:c25
isempty :: nil:add -> true:false
low :: 0':s -> nil:add -> nil:add
head :: nil:add -> 0':s
tail :: nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c18 :: c23:c24:c25 -> c5:c6 -> c13 -> c17:c18:c19:c20:c21:c22
c19 :: c23:c24:c25 -> c5:c6 -> c14 -> c17:c18:c19:c20:c21:c22
c20 :: c23:c24:c25 -> c13 -> c17:c18:c19:c20:c21:c22
c21 :: c23:c24:c25 -> c9:c10 -> c13 -> c17:c18:c19:c20:c21:c22
c22 :: c23:c24:c25 -> c9:c10 -> c14 -> c17:c18:c19:c20:c21:c22
c23 :: c23:c24:c25
c24 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
quicksort :: nil:add -> nil:add
c25 :: c3:c4 -> c17:c18:c19:c20:c21:c22 -> c23:c24:c25
app :: nil:add -> nil:add -> nil:add
if_low :: true:false -> 0':s -> nil:add -> nil:add
if_high :: true:false -> 0':s -> nil:add -> nil:add
if_qs :: true:false -> nil:add -> 0':s -> nil:add -> nil:add
hole_c:c1:c21_26 :: c:c1:c2
hole_0':s2_26 :: 0':s
hole_c3:c43_26 :: c3:c4
hole_nil:add4_26 :: nil:add
hole_c5:c65_26 :: c5:c6
hole_c7:c86_26 :: c7:c8
hole_true:false7_26 :: true:false
hole_c9:c108_26 :: c9:c10
hole_c11:c129_26 :: c11:c12
hole_c1310_26 :: c13
hole_c1411_26 :: c14
hole_c15:c1612_26 :: c15:c16
hole_c17:c18:c19:c20:c21:c2213_26 :: c17:c18:c19:c20:c21:c22
hole_c23:c24:c2514_26 :: c23:c24:c25
gen_c:c1:c215_26 :: Nat -> c:c1:c2
gen_0':s16_26 :: Nat -> 0':s
gen_c3:c417_26 :: Nat -> c3:c4
gen_nil:add18_26 :: Nat -> nil:add


Lemmas:
LE(gen_0':s16_26(n20_26), gen_0':s16_26(n20_26)) -> gen_c:c1:c215_26(n20_26), rt in Omega(1 + n20_26)
APP(gen_nil:add18_26(n754_26), gen_nil:add18_26(b)) -> gen_c3:c417_26(n754_26), rt in Omega(1 + n754_26)
le(gen_0':s16_26(n1772_26), gen_0':s16_26(n1772_26)) -> true, rt in Omega(0)
LOW(gen_0':s16_26(0), gen_nil:add18_26(n2265_26)) -> *19_26, rt in Omega(n2265_26)
HIGH(gen_0':s16_26(0), gen_nil:add18_26(n7047_26)) -> *19_26, rt in Omega(n7047_26)
low(gen_0':s16_26(0), gen_nil:add18_26(n14737_26)) -> gen_nil:add18_26(n14737_26), rt in Omega(0)
high(gen_0':s16_26(0), gen_nil:add18_26(n16288_26)) -> gen_nil:add18_26(0), rt in Omega(0)
app(gen_nil:add18_26(n17743_26), gen_nil:add18_26(b)) -> gen_nil:add18_26(+(n17743_26, b)), rt in Omega(0)
quicksort(gen_nil:add18_26(n20042_26)) -> gen_nil:add18_26(n20042_26), rt in Omega(0)


Generator Equations:
gen_c:c1:c215_26(0) <=> c
gen_c:c1:c215_26(+(x, 1)) <=> c2(gen_c:c1:c215_26(x))
gen_0':s16_26(0) <=> 0'
gen_0':s16_26(+(x, 1)) <=> s(gen_0':s16_26(x))
gen_c3:c417_26(0) <=> c3
gen_c3:c417_26(+(x, 1)) <=> c4(gen_c3:c417_26(x))
gen_nil:add18_26(0) <=> nil
gen_nil:add18_26(+(x, 1)) <=> add(0', gen_nil:add18_26(x))


The following defined symbols remain to be analysed:
QUICKSORT
----------------------------------------

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

(36)
BOUNDS(n^2, INF)