WORST_CASE(Omega(n^2),?)
proof of input_Q07Xxt3Z0K.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), 4 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 377 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), 72 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 165 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 65 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 44 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 700 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 683 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
        (30) typed CpxTrs
        (31) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
        (32) typed CpxTrs
        (33) RewriteLemmaProof [LOWER BOUND(ID), 72 ms]
        (34) typed CpxTrs
        (35) RewriteLemmaProof [LOWER BOUND(ID), 83 ms]
        (36) typed CpxTrs
        (37) RewriteLemmaProof [LOWER BOUND(ID), 427 ms]
        (38) proven lower bound
        (39) LowerBoundPropagationProof [FINISHED, 0 ms]
        (40) 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:

   minus(x, 0) -> x
   minus(s(x), s(y)) -> minus(x, y)
   quot(0, s(y)) -> 0
   quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
   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))
   quicksort(nil) -> nil
   quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

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:
   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   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))
   quicksort(nil) -> nil
   quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))
Tuples:
   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   LOW(z0, nil) -> c9
   LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
   HIGH(z0, nil) -> c13
   HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
   QUICKSORT(nil) -> c17
   QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
   QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
S tuples:
   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   LOW(z0, nil) -> c9
   LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
   HIGH(z0, nil) -> c13
   HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
   QUICKSORT(nil) -> c17
   QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
   QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
K tuples:none
Defined Rule Symbols:   minus_2, quot_2, le_2, app_2, low_2, if_low_3, high_2, if_high_3, quicksort_1

Defined Pair Symbols:   MINUS_2, QUOT_2, LE_2, APP_2, LOW_2, IF_LOW_3, HIGH_2, IF_HIGH_3, QUICKSORT_1

Compound Symbols:   c, c1_1, c2, c3_2, c4, c5, c6_1, c7, c8_1, c9, c10_2, c11_1, c12_1, c13, c14_2, c15_1, c16_1, c17, c18_3, c19_3


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

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

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   LOW(z0, nil) -> c9
   LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
   HIGH(z0, nil) -> c13
   HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
   QUICKSORT(nil) -> c17
   QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
   QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   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))
   quicksort(nil) -> nil
   quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

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:

   MINUS(z0, 0') -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c2
   QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   LE(0', z0) -> c4
   LE(s(z0), 0') -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   APP(nil, z0) -> c7
   APP(add(z0, z1), z2) -> c8(APP(z1, z2))
   LOW(z0, nil) -> c9
   LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
   IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
   HIGH(z0, nil) -> c13
   HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
   IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
   IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
   QUICKSORT(nil) -> c17
   QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
   QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))

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

   minus(z0, 0') -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   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))
   quicksort(nil) -> nil
   quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19

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

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

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

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

(10)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)

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

Induction Step:
MINUS(gen_0':s14_20(+(n21_20, 1)), gen_0':s14_20(+(n21_20, 1))) ->_R^Omega(1)
c1(MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20))) ->_IH
c1(gen_c:c113_20(c22_20))

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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)

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

Induction Step:
minus(gen_0':s14_20(+(n569_20, 1)), gen_0':s14_20(+(n569_20, 1))) ->_R^Omega(0)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) ->_IH
gen_0':s14_20(0)

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

(18)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


The following defined symbols remain to be analysed:
QUOT, LE, APP, LOW, le, HIGH, QUICKSORT, quicksort, low, high, quot, 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
quicksort < QUICKSORT
low < QUICKSORT
high < QUICKSORT
low < quicksort
high < quicksort
app < quicksort

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)

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

Induction Step:
LE(gen_0':s14_20(+(n2545_20, 1)), gen_0':s14_20(+(n2545_20, 1))) ->_R^Omega(1)
c6(LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20))) ->_IH
c6(gen_c4:c5:c616_20(c2546_20))

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

(20)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)

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

Induction Step:
APP(gen_nil:add18_20(+(n3394_20, 1)), gen_nil:add18_20(b)) ->_R^Omega(1)
c8(APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b))) ->_IH
c8(gen_c7:c817_20(c3395_20))

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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)

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

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

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

(24)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)

Induction Base:
LOW(gen_0':s14_20(0), gen_nil:add18_20(0))

Induction Step:
LOW(gen_0':s14_20(0), gen_nil:add18_20(+(n4944_20, 1))) ->_R^Omega(1)
c10(IF_LOW(le(0', gen_0':s14_20(0)), gen_0':s14_20(0), add(0', gen_nil:add18_20(n4944_20))), LE(0', gen_0':s14_20(0))) ->_L^Omega(0)
c10(IF_LOW(true, gen_0':s14_20(0), add(0', gen_nil:add18_20(n4944_20))), LE(0', gen_0':s14_20(0))) ->_R^Omega(1)
c10(c11(LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20))), LE(0', gen_0':s14_20(0))) ->_IH
c10(c11(*20_20), LE(0', gen_0':s14_20(0))) ->_L^Omega(1)
c10(c11(*20_20), gen_c4:c5:c616_20(0))

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

(26)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)

Induction Base:
HIGH(gen_0':s14_20(0), gen_nil:add18_20(0))

Induction Step:
HIGH(gen_0':s14_20(0), gen_nil:add18_20(+(n12207_20, 1))) ->_R^Omega(1)
c14(IF_HIGH(le(0', gen_0':s14_20(0)), gen_0':s14_20(0), add(0', gen_nil:add18_20(n12207_20))), LE(0', gen_0':s14_20(0))) ->_L^Omega(0)
c14(IF_HIGH(true, gen_0':s14_20(0), add(0', gen_nil:add18_20(n12207_20))), LE(0', gen_0':s14_20(0))) ->_R^Omega(1)
c14(c15(HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20))), LE(0', gen_0':s14_20(0))) ->_IH
c14(c15(*20_20), LE(0', gen_0':s14_20(0))) ->_L^Omega(1)
c14(c15(*20_20), gen_c4:c5:c616_20(0))

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

(28)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)

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

Induction Step:
low(gen_0':s14_20(0), gen_nil:add18_20(+(n22378_20, 1))) ->_R^Omega(0)
if_low(le(0', gen_0':s14_20(0)), gen_0':s14_20(0), add(0', gen_nil:add18_20(n22378_20))) ->_L^Omega(0)
if_low(true, gen_0':s14_20(0), add(0', gen_nil:add18_20(n22378_20))) ->_R^Omega(0)
add(0', low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20))) ->_IH
add(0', gen_nil:add18_20(c22379_20))

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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
high(gen_0':s14_20(0), gen_nil:add18_20(n23944_20)) -> gen_nil:add18_20(0), rt in Omega(0)

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

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

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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)
high(gen_0':s14_20(0), gen_nil:add18_20(n23944_20)) -> gen_nil:add18_20(0), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
app(gen_nil:add18_20(n25774_20), gen_nil:add18_20(b)) -> gen_nil:add18_20(+(n25774_20, b)), rt in Omega(0)

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

Induction Step:
app(gen_nil:add18_20(+(n25774_20, 1)), gen_nil:add18_20(b)) ->_R^Omega(0)
add(0', app(gen_nil:add18_20(n25774_20), gen_nil:add18_20(b))) ->_IH
add(0', gen_nil:add18_20(+(b, c25775_20)))

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

(34)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)
high(gen_0':s14_20(0), gen_nil:add18_20(n23944_20)) -> gen_nil:add18_20(0), rt in Omega(0)
app(gen_nil:add18_20(n25774_20), gen_nil:add18_20(b)) -> gen_nil:add18_20(+(n25774_20, b)), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
quicksort(gen_nil:add18_20(n28473_20)) -> gen_nil:add18_20(n28473_20), rt in Omega(0)

Induction Base:
quicksort(gen_nil:add18_20(0)) ->_R^Omega(0)
nil

Induction Step:
quicksort(gen_nil:add18_20(+(n28473_20, 1))) ->_R^Omega(0)
app(quicksort(low(0', gen_nil:add18_20(n28473_20))), add(0', quicksort(high(0', gen_nil:add18_20(n28473_20))))) ->_L^Omega(0)
app(quicksort(gen_nil:add18_20(n28473_20)), add(0', quicksort(high(0', gen_nil:add18_20(n28473_20))))) ->_IH
app(gen_nil:add18_20(c28474_20), add(0', quicksort(high(0', gen_nil:add18_20(n28473_20))))) ->_L^Omega(0)
app(gen_nil:add18_20(n28473_20), add(0', quicksort(gen_nil:add18_20(0)))) ->_R^Omega(0)
app(gen_nil:add18_20(n28473_20), add(0', nil)) ->_L^Omega(0)
gen_nil:add18_20(+(n28473_20, +(0, 1)))

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

(36)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)
high(gen_0':s14_20(0), gen_nil:add18_20(n23944_20)) -> gen_nil:add18_20(0), rt in Omega(0)
app(gen_nil:add18_20(n25774_20), gen_nil:add18_20(b)) -> gen_nil:add18_20(+(n25774_20, b)), rt in Omega(0)
quicksort(gen_nil:add18_20(n28473_20)) -> gen_nil:add18_20(n28473_20), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
QUICKSORT(gen_nil:add18_20(n30263_20)) -> *20_20, rt in Omega(n30263_20 + n30263_20^2)

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

Induction Step:
QUICKSORT(gen_nil:add18_20(+(n30263_20, 1))) ->_R^Omega(1)
c18(APP(quicksort(low(0', gen_nil:add18_20(n30263_20))), add(0', quicksort(high(0', gen_nil:add18_20(n30263_20))))), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(0)
c18(APP(quicksort(gen_nil:add18_20(n30263_20)), add(0', quicksort(high(0', gen_nil:add18_20(n30263_20))))), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(0)
c18(APP(gen_nil:add18_20(n30263_20), add(0', quicksort(high(0', gen_nil:add18_20(n30263_20))))), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(0)
c18(APP(gen_nil:add18_20(n30263_20), add(0', quicksort(gen_nil:add18_20(0)))), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(0)
c18(APP(gen_nil:add18_20(n30263_20), add(0', gen_nil:add18_20(0))), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(1 + n30263_20)
c18(gen_c7:c817_20(n30263_20), QUICKSORT(low(0', gen_nil:add18_20(n30263_20))), LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(0)
c18(gen_c7:c817_20(n30263_20), QUICKSORT(gen_nil:add18_20(n30263_20)), LOW(0', gen_nil:add18_20(n30263_20))) ->_IH
c18(gen_c7:c817_20(n30263_20), *20_20, LOW(0', gen_nil:add18_20(n30263_20))) ->_L^Omega(n30263_20)
c18(gen_c7:c817_20(n30263_20), *20_20, *20_20)

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

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

Innermost TRS:
Rules:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
QUOT(0', s(z0)) -> c2
QUOT(s(z0), s(z1)) -> c3(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
APP(nil, z0) -> c7
APP(add(z0, z1), z2) -> c8(APP(z1, z2))
LOW(z0, nil) -> c9
LOW(z0, add(z1, z2)) -> c10(IF_LOW(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_LOW(true, z0, add(z1, z2)) -> c11(LOW(z0, z2))
IF_LOW(false, z0, add(z1, z2)) -> c12(LOW(z0, z2))
HIGH(z0, nil) -> c13
HIGH(z0, add(z1, z2)) -> c14(IF_HIGH(le(z1, z0), z0, add(z1, z2)), LE(z1, z0))
IF_HIGH(true, z0, add(z1, z2)) -> c15(HIGH(z0, z2))
IF_HIGH(false, z0, add(z1, z2)) -> c16(HIGH(z0, z2))
QUICKSORT(nil) -> c17
QUICKSORT(add(z0, z1)) -> c18(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(low(z0, z1)), LOW(z0, z1))
QUICKSORT(add(z0, z1)) -> c19(APP(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1)))), QUICKSORT(high(z0, z1)), HIGH(z0, z1))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
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))
quicksort(nil) -> nil
quicksort(add(z0, z1)) -> app(quicksort(low(z0, z1)), add(z0, quicksort(high(z0, z1))))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
QUOT :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
minus :: 0':s -> 0':s -> 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
APP :: nil:add -> nil:add -> c7:c8
nil :: nil:add
c7 :: c7:c8
add :: 0':s -> nil:add -> nil:add
c8 :: c7:c8 -> c7:c8
LOW :: 0':s -> nil:add -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c4:c5:c6 -> c9:c10
IF_LOW :: true:false -> 0':s -> nil:add -> c11:c12
le :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c9:c10 -> c11:c12
false :: true:false
c12 :: c9:c10 -> c11:c12
HIGH :: 0':s -> nil:add -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c4:c5:c6 -> c13:c14
IF_HIGH :: true:false -> 0':s -> nil:add -> c15:c16
c15 :: c13:c14 -> c15:c16
c16 :: c13:c14 -> c15:c16
QUICKSORT :: nil:add -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c7:c8 -> c17:c18:c19 -> c9:c10 -> c17:c18:c19
quicksort :: nil:add -> nil:add
low :: 0':s -> nil:add -> nil:add
high :: 0':s -> nil:add -> nil:add
c19 :: c7:c8 -> c17:c18:c19 -> c13:c14 -> c17:c18:c19
quot :: 0':s -> 0':s -> 0':s
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
hole_c:c11_20 :: c:c1
hole_0':s2_20 :: 0':s
hole_c2:c33_20 :: c2:c3
hole_c4:c5:c64_20 :: c4:c5:c6
hole_c7:c85_20 :: c7:c8
hole_nil:add6_20 :: nil:add
hole_c9:c107_20 :: c9:c10
hole_c11:c128_20 :: c11:c12
hole_true:false9_20 :: true:false
hole_c13:c1410_20 :: c13:c14
hole_c15:c1611_20 :: c15:c16
hole_c17:c18:c1912_20 :: c17:c18:c19
gen_c:c113_20 :: Nat -> c:c1
gen_0':s14_20 :: Nat -> 0':s
gen_c2:c315_20 :: Nat -> c2:c3
gen_c4:c5:c616_20 :: Nat -> c4:c5:c6
gen_c7:c817_20 :: Nat -> c7:c8
gen_nil:add18_20 :: Nat -> nil:add
gen_c17:c18:c1919_20 :: Nat -> c17:c18:c19


Lemmas:
MINUS(gen_0':s14_20(n21_20), gen_0':s14_20(n21_20)) -> gen_c:c113_20(n21_20), rt in Omega(1 + n21_20)
minus(gen_0':s14_20(n569_20), gen_0':s14_20(n569_20)) -> gen_0':s14_20(0), rt in Omega(0)
LE(gen_0':s14_20(n2545_20), gen_0':s14_20(n2545_20)) -> gen_c4:c5:c616_20(n2545_20), rt in Omega(1 + n2545_20)
APP(gen_nil:add18_20(n3394_20), gen_nil:add18_20(b)) -> gen_c7:c817_20(n3394_20), rt in Omega(1 + n3394_20)
le(gen_0':s14_20(n4451_20), gen_0':s14_20(n4451_20)) -> true, rt in Omega(0)
LOW(gen_0':s14_20(0), gen_nil:add18_20(n4944_20)) -> *20_20, rt in Omega(n4944_20)
HIGH(gen_0':s14_20(0), gen_nil:add18_20(n12207_20)) -> *20_20, rt in Omega(n12207_20)
low(gen_0':s14_20(0), gen_nil:add18_20(n22378_20)) -> gen_nil:add18_20(n22378_20), rt in Omega(0)
high(gen_0':s14_20(0), gen_nil:add18_20(n23944_20)) -> gen_nil:add18_20(0), rt in Omega(0)
app(gen_nil:add18_20(n25774_20), gen_nil:add18_20(b)) -> gen_nil:add18_20(+(n25774_20, b)), rt in Omega(0)
quicksort(gen_nil:add18_20(n28473_20)) -> gen_nil:add18_20(n28473_20), rt in Omega(0)


Generator Equations:
gen_c:c113_20(0) <=> c
gen_c:c113_20(+(x, 1)) <=> c1(gen_c:c113_20(x))
gen_0':s14_20(0) <=> 0'
gen_0':s14_20(+(x, 1)) <=> s(gen_0':s14_20(x))
gen_c2:c315_20(0) <=> c2
gen_c2:c315_20(+(x, 1)) <=> c3(gen_c2:c315_20(x), c)
gen_c4:c5:c616_20(0) <=> c4
gen_c4:c5:c616_20(+(x, 1)) <=> c6(gen_c4:c5:c616_20(x))
gen_c7:c817_20(0) <=> c7
gen_c7:c817_20(+(x, 1)) <=> c8(gen_c7:c817_20(x))
gen_nil:add18_20(0) <=> nil
gen_nil:add18_20(+(x, 1)) <=> add(0', gen_nil:add18_20(x))
gen_c17:c18:c1919_20(0) <=> c17
gen_c17:c18:c1919_20(+(x, 1)) <=> c18(c7, gen_c17:c18:c1919_20(x), c9)


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

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

(40)
BOUNDS(n^2, INF)