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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 489 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 27 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 0 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 342 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 139 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 20 ms]
(18) BEST
    (19) proven lower bound
        (20) LowerBoundPropagationProof [FINISHED, 0 ms]
        (21) BOUNDS(n^1, INF)
    (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 144 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 7 ms]
        (28) typed CpxTrs


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

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


The TRS R consists of the following rules:

   quicksort(Cons(x, Cons(x', xs))) -> part(x, Cons(x, Cons(x', xs)), Cons(x, Nil), Nil)
   quicksort(Cons(x, Nil)) -> Cons(x, Nil)
   quicksort(Nil) -> Nil
   part(x', Cons(x, xs), xs1, xs2) -> part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)
   part(x, Nil, xs1, xs2) -> app(quicksort(xs1), quicksort(xs2))
   app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
   app(Nil, ys) -> ys
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   goal(xs) -> quicksort(xs)

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

   <(S(x), S(y)) -> <(x, y)
   <(0, S(y)) -> True
   <(x, 0) -> False
   >(S(x), S(y)) -> >(x, y)
   >(0, y) -> False
   >(S(x), 0) -> True
   part[Ite][True][Ite](True, x', Cons(x, xs), xs1, xs2) -> part(x', xs, Cons(x, xs1), xs2)
   part[Ite][True][Ite](False, x', Cons(x, xs), xs1, xs2) -> part[Ite][True][Ite][False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

   quicksort(Cons(x, Cons(x', xs))) -> part(x, Cons(x, Cons(x', xs)), Cons(x, Nil), Nil)
   quicksort(Cons(x, Nil)) -> Cons(x, Nil)
   quicksort(Nil) -> Nil
   part(x', Cons(x, xs), xs1, xs2) -> part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)
   part(x, Nil, xs1, xs2) -> app(quicksort(xs1), quicksort(xs2))
   app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
   app(Nil, ys) -> ys
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   goal(xs) -> quicksort(xs)

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

   <(S(x), S(y)) -> <(x, y)
   <(0, S(y)) -> True
   <(x, 0) -> False
   >(S(x), S(y)) -> >(x, y)
   >(0, y) -> False
   >(S(x), 0) -> True
   part[Ite][True][Ite](True, x', Cons(x, xs), xs1, xs2) -> part(x', xs, Cons(x, xs1), xs2)
   part[Ite][True][Ite](False, x', Cons(x, xs), xs1, xs2) -> part[Ite][True][Ite][False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0, S(z0)) -> True
   <(z0, 0) -> False
   >(S(z0), S(z1)) -> >(z0, z1)
   >(0, z0) -> False
   >(S(z0), 0) -> True
   part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
   part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
   quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
   quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
   quicksort(Nil) -> Nil
   part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
   part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
   app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
   app(Nil, z0) -> z0
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   goal(z0) -> quicksort(z0)
Tuples:
   <'(S(z0), S(z1)) -> c(<'(z0, z1))
   <'(0, S(z0)) -> c1
   <'(z0, 0) -> c2
   >'(S(z0), S(z1)) -> c3(>'(z0, z1))
   >'(0, z0) -> c4
   >'(S(z0), 0) -> c5
   PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
   PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
   QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
   QUICKSORT(Cons(z0, Nil)) -> c9
   QUICKSORT(Nil) -> c10
   PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
   PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
   PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
   APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
   APP(Nil, z0) -> c15
   NOTEMPTY(Cons(z0, z1)) -> c16
   NOTEMPTY(Nil) -> c17
   GOAL(z0) -> c18(QUICKSORT(z0))
S tuples:
   QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
   QUICKSORT(Cons(z0, Nil)) -> c9
   QUICKSORT(Nil) -> c10
   PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
   PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
   PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
   APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
   APP(Nil, z0) -> c15
   NOTEMPTY(Cons(z0, z1)) -> c16
   NOTEMPTY(Nil) -> c17
   GOAL(z0) -> c18(QUICKSORT(z0))
K tuples:none
Defined Rule Symbols:   quicksort_1, part_4, app_2, notEmpty_1, goal_1, <_2, >_2, part[Ite][True][Ite]_5

Defined Pair Symbols:   <'_2, >'_2, PART[ITE][TRUE][ITE]_5, QUICKSORT_1, PART_4, APP_2, NOTEMPTY_1, GOAL_1

Compound Symbols:   c_1, c1, c2, c3_1, c4, c5, c6_1, c7_1, c8_1, c9, c10, c11_2, c12_2, c13_2, c14_1, c15, c16, c17, c18_1


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

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

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


The TRS R consists of the following rules:

   QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
   QUICKSORT(Cons(z0, Nil)) -> c9
   QUICKSORT(Nil) -> c10
   PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
   PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
   PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
   APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
   APP(Nil, z0) -> c15
   NOTEMPTY(Cons(z0, z1)) -> c16
   NOTEMPTY(Nil) -> c17
   GOAL(z0) -> c18(QUICKSORT(z0))

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

   <'(S(z0), S(z1)) -> c(<'(z0, z1))
   <'(0, S(z0)) -> c1
   <'(z0, 0) -> c2
   >'(S(z0), S(z1)) -> c3(>'(z0, z1))
   >'(0, z0) -> c4
   >'(S(z0), 0) -> c5
   PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
   PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0, S(z0)) -> True
   <(z0, 0) -> False
   >(S(z0), S(z1)) -> >(z0, z1)
   >(0, z0) -> False
   >(S(z0), 0) -> True
   part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
   part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
   quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
   quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
   quicksort(Nil) -> Nil
   part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
   part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
   app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
   app(Nil, z0) -> z0
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   goal(z0) -> quicksort(z0)

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

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

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


The TRS R consists of the following rules:

   QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
   QUICKSORT(Cons(z0, Nil)) -> c9
   QUICKSORT(Nil) -> c10
   PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
   PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
   PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
   APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
   APP(Nil, z0) -> c15
   NOTEMPTY(Cons(z0, z1)) -> c16
   NOTEMPTY(Nil) -> c17
   GOAL(z0) -> c18(QUICKSORT(z0))

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

   <'(S(z0), S(z1)) -> c(<'(z0, z1))
   <'(0', S(z0)) -> c1
   <'(z0, 0') -> c2
   >'(S(z0), S(z1)) -> c3(>'(z0, z1))
   >'(0', z0) -> c4
   >'(S(z0), 0') -> c5
   PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
   PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
   <(S(z0), S(z1)) -> <(z0, z1)
   <(0', S(z0)) -> True
   <(z0, 0') -> False
   >(S(z0), S(z1)) -> >(z0, z1)
   >(0', z0) -> False
   >(S(z0), 0') -> True
   part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
   part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
   quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
   quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
   quicksort(Nil) -> Nil
   part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
   part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
   app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
   app(Nil, z0) -> z0
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   goal(z0) -> quicksort(z0)

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

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

(10)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
QUICKSORT, PART, >, >', APP, quicksort, <', <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
> < PART
>' < PART
APP < PART
quicksort < PART
<' < PART
> < part
quicksort = part
< < part
app < part

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

(12)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


The following defined symbols remain to be analysed:
>, QUICKSORT, PART, >', APP, quicksort, <', <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
> < PART
>' < PART
APP < PART
quicksort < PART
<' < PART
> < part
quicksort = part
< < part
app < part

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)

Induction Base:
>(gen_S:0'13_19(0), gen_S:0'13_19(0)) ->_R^Omega(0)
False

Induction Step:
>(gen_S:0'13_19(+(n18_19, 1)), gen_S:0'13_19(+(n18_19, 1))) ->_R^Omega(0)
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) ->_IH
False

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

(14)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


The following defined symbols remain to be analysed:
>', QUICKSORT, PART, APP, quicksort, <', <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
>' < PART
APP < PART
quicksort < PART
<' < PART
quicksort = part
< < part
app < part

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)

Induction Base:
>'(gen_S:0'13_19(0), gen_S:0'13_19(0)) ->_R^Omega(0)
c4

Induction Step:
>'(gen_S:0'13_19(+(n407_19, 1)), gen_S:0'13_19(+(n407_19, 1))) ->_R^Omega(0)
c3(>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19))) ->_IH
c3(gen_c3:c4:c514_19(c408_19))

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

(16)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


The following defined symbols remain to be analysed:
APP, QUICKSORT, PART, quicksort, <', <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
APP < PART
quicksort < PART
<' < PART
quicksort = part
< < part
app < part

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_c14:c1515_19(n1121_19), rt in Omega(1 + n1121_19)

Induction Base:
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) ->_R^Omega(1)
c15

Induction Step:
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(n1121_19, 1)), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) ->_R^Omega(1)
c14(APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b))) ->_IH
c14(gen_c14:c1515_19(c1122_19))

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

(18)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


The following defined symbols remain to be analysed:
APP, QUICKSORT, PART, quicksort, <', <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
APP < PART
quicksort < PART
<' < PART
quicksort = part
< < part
app < part

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

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

(21)
BOUNDS(n^1, INF)

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

(22)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_c14:c1515_19(n1121_19), rt in Omega(1 + n1121_19)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


The following defined symbols remain to be analysed:
<', QUICKSORT, PART, quicksort, <, part, app

They will be analysed ascendingly in the following order:
QUICKSORT = PART
quicksort < PART
<' < PART
quicksort = part
< < part
app < part

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<'(gen_S:0'13_19(n2043_19), gen_S:0'13_19(+(1, n2043_19))) -> gen_c:c1:c216_19(n2043_19), rt in Omega(0)

Induction Base:
<'(gen_S:0'13_19(0), gen_S:0'13_19(+(1, 0))) ->_R^Omega(0)
c1

Induction Step:
<'(gen_S:0'13_19(+(n2043_19, 1)), gen_S:0'13_19(+(1, +(n2043_19, 1)))) ->_R^Omega(0)
c(<'(gen_S:0'13_19(n2043_19), gen_S:0'13_19(+(1, n2043_19)))) ->_IH
c(gen_c:c1:c216_19(c2044_19))

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:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_c14:c1515_19(n1121_19), rt in Omega(1 + n1121_19)
<'(gen_S:0'13_19(n2043_19), gen_S:0'13_19(+(1, n2043_19))) -> gen_c:c1:c216_19(n2043_19), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


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

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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<(gen_S:0'13_19(n2832_19), gen_S:0'13_19(+(1, n2832_19))) -> True, rt in Omega(0)

Induction Base:
<(gen_S:0'13_19(0), gen_S:0'13_19(+(1, 0))) ->_R^Omega(0)
True

Induction Step:
<(gen_S:0'13_19(+(n2832_19, 1)), gen_S:0'13_19(+(1, +(n2832_19, 1)))) ->_R^Omega(0)
<(gen_S:0'13_19(n2832_19), gen_S:0'13_19(+(1, n2832_19))) ->_IH
True

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

(26)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_c14:c1515_19(n1121_19), rt in Omega(1 + n1121_19)
<'(gen_S:0'13_19(n2043_19), gen_S:0'13_19(+(1, n2043_19))) -> gen_c:c1:c216_19(n2043_19), rt in Omega(0)
<(gen_S:0'13_19(n2832_19), gen_S:0'13_19(+(1, n2832_19))) -> True, rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


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

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

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
app(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n3238_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(n3238_19, b)), rt in Omega(0)

Induction Base:
app(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) ->_R^Omega(0)
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)

Induction Step:
app(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(n3238_19, 1)), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) ->_R^Omega(0)
Cons(0', app(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n3238_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b))) ->_IH
Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(b, c3239_19)))

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

(28)
Obligation:
Innermost TRS:
Rules:
QUICKSORT(Cons(z0, Cons(z1, z2))) -> c8(PART(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil))
QUICKSORT(Cons(z0, Nil)) -> c9
QUICKSORT(Nil) -> c10
PART(z0, Cons(z1, z2), z3, z4) -> c11(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
PART(z0, Nil, z1, z2) -> c12(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z1))
PART(z0, Nil, z1, z2) -> c13(APP(quicksort(z1), quicksort(z2)), QUICKSORT(z2))
APP(Cons(z0, z1), z2) -> c14(APP(z1, z2))
APP(Nil, z0) -> c15
NOTEMPTY(Cons(z0, z1)) -> c16
NOTEMPTY(Nil) -> c17
GOAL(z0) -> c18(QUICKSORT(z0))
<'(S(z0), S(z1)) -> c(<'(z0, z1))
<'(0', S(z0)) -> c1
<'(z0, 0') -> c2
>'(S(z0), S(z1)) -> c3(>'(z0, z1))
>'(0', z0) -> c4
>'(S(z0), 0') -> c5
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) -> c6(PART(z0, z2, Cons(z1, z3), z4))
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) -> c7(<'(z0, z1))
<(S(z0), S(z1)) -> <(z0, z1)
<(0', S(z0)) -> True
<(z0, 0') -> False
>(S(z0), S(z1)) -> >(z0, z1)
>(0', z0) -> False
>(S(z0), 0') -> True
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) -> part(z0, z2, Cons(z1, z3), z4)
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4)
quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z0, Cons(z1, z2)), Cons(z0, Nil), Nil)
quicksort(Cons(z0, Nil)) -> Cons(z0, Nil)
quicksort(Nil) -> Nil
part(z0, Cons(z1, z2), z3, z4) -> part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4)
part(z0, Nil, z1, z2) -> app(quicksort(z1), quicksort(z2))
app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2))
app(Nil, z0) -> z0
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
goal(z0) -> quicksort(z0)

Types:
QUICKSORT :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c8:c9:c10
Cons :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c8 :: c11:c12:c13 -> c8:c9:c10
PART :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c11:c12:c13
Nil :: Cons:Nil:part[Ite][True][Ite][False][Ite]
c9 :: c8:c9:c10
c10 :: c8:c9:c10
c11 :: c6:c7 -> c3:c4:c5 -> c11:c12:c13
PART[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c6:c7
> :: S:0' -> S:0' -> True:False
>' :: S:0' -> S:0' -> c3:c4:c5
c12 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
APP :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> c14:c15
quicksort :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
c13 :: c14:c15 -> c8:c9:c10 -> c11:c12:c13
c14 :: c14:c15 -> c14:c15
c15 :: c14:c15
NOTEMPTY :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c16:c17
c16 :: c16:c17
c17 :: c16:c17
GOAL :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> c18
c18 :: c8:c9:c10 -> c18
<' :: S:0' -> S:0' -> c:c1:c2
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
True :: True:False
c6 :: c11:c12:c13 -> c6:c7
False :: True:False
c7 :: c:c1:c2 -> c6:c7
< :: S:0' -> S:0' -> True:False
part[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part :: S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
part[Ite][True][Ite][False][Ite] :: True:False -> S:0' -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
app :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
notEmpty :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> True:False
goal :: Cons:Nil:part[Ite][True][Ite][False][Ite] -> Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_c8:c9:c101_19 :: c8:c9:c10
hole_Cons:Nil:part[Ite][True][Ite][False][Ite]2_19 :: Cons:Nil:part[Ite][True][Ite][False][Ite]
hole_S:0'3_19 :: S:0'
hole_c11:c12:c134_19 :: c11:c12:c13
hole_c6:c75_19 :: c6:c7
hole_c3:c4:c56_19 :: c3:c4:c5
hole_True:False7_19 :: True:False
hole_c14:c158_19 :: c14:c15
hole_c16:c179_19 :: c16:c17
hole_c1810_19 :: c18
hole_c:c1:c211_19 :: c:c1:c2
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19 :: Nat -> Cons:Nil:part[Ite][True][Ite][False][Ite]
gen_S:0'13_19 :: Nat -> S:0'
gen_c3:c4:c514_19 :: Nat -> c3:c4:c5
gen_c14:c1515_19 :: Nat -> c14:c15
gen_c:c1:c216_19 :: Nat -> c:c1:c2


Lemmas:
>(gen_S:0'13_19(n18_19), gen_S:0'13_19(n18_19)) -> False, rt in Omega(0)
>'(gen_S:0'13_19(n407_19), gen_S:0'13_19(n407_19)) -> gen_c3:c4:c514_19(n407_19), rt in Omega(0)
APP(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n1121_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_c14:c1515_19(n1121_19), rt in Omega(1 + n1121_19)
<'(gen_S:0'13_19(n2043_19), gen_S:0'13_19(+(1, n2043_19))) -> gen_c:c1:c216_19(n2043_19), rt in Omega(0)
<(gen_S:0'13_19(n2832_19), gen_S:0'13_19(+(1, n2832_19))) -> True, rt in Omega(0)
app(gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(n3238_19), gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(b)) -> gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(n3238_19, b)), rt in Omega(0)


Generator Equations:
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(0) <=> Nil
gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(+(x, 1)) <=> Cons(0', gen_Cons:Nil:part[Ite][True][Ite][False][Ite]12_19(x))
gen_S:0'13_19(0) <=> 0'
gen_S:0'13_19(+(x, 1)) <=> S(gen_S:0'13_19(x))
gen_c3:c4:c514_19(0) <=> c4
gen_c3:c4:c514_19(+(x, 1)) <=> c3(gen_c3:c4:c514_19(x))
gen_c14:c1515_19(0) <=> c15
gen_c14:c1515_19(+(x, 1)) <=> c14(gen_c14:c1515_19(x))
gen_c:c1:c216_19(0) <=> c1
gen_c:c1:c216_19(+(x, 1)) <=> c(gen_c:c1:c216_19(x))


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

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