WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(Cons(z0,z1),z2) -> c17(APP(z1,z2))
            APP(Nil(),z0) -> c18()
            GOAL(z0) -> c23(QUICKSORT(z0))
            NOTEMPTY(Cons(z0,z1)) -> c19()
            NOTEMPTY(Nil()) -> c20()
            PART(z0,z1) -> c21(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partLt(z0,z1))
                              ,PARTLT(z0,z1))
            PART(z0,z1) -> c22(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partGt(z0,z1))
                              ,PARTGT(z0,z1))
            PARTGT(z0,Cons(z1,z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1,z0),z0,Cons(z1,z2)),>'(z1,z0))
            PARTGT(z0,Nil()) -> c16()
            PARTLT(z0,Cons(z1,z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1,z0),z0,Cons(z1,z2)),<'(z1,z0))
            PARTLT(z0,Nil()) -> c14()
            QUICKSORT(Cons(z0,Cons(z1,z2))) -> c10(PART(z0,Cons(z1,z2)))
            QUICKSORT(Cons(z0,Nil())) -> c11()
            QUICKSORT(Nil()) -> c12()
        - Weak TRS:
            <(z0,0()) -> False()
            <(0(),S(z0)) -> True()
            <(S(z0),S(z1)) -> <(z0,z1)
            <'(z0,0()) -> c2()
            <'(0(),S(z0)) -> c1()
            <'(S(z0),S(z1)) -> c(<'(z0,z1))
            >(0(),z0) -> False()
            >(S(z0),0()) -> True()
            >(S(z0),S(z1)) -> >(z0,z1)
            >'(0(),z0) -> c4()
            >'(S(z0),0()) -> c5()
            >'(S(z0),S(z1)) -> c3(>'(z0,z1))
            PARTGT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c9(PARTGT(z0,z2))
            PARTGT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c8(PARTGT(z0,z2))
            PARTLT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c7(PARTLT(z0,z2))
            PARTLT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c6(PARTLT(z0,z2))
            app(Cons(z0,z1),z2) -> Cons(z0,app(z1,z2))
            app(Nil(),z0) -> z0
            goal(z0) -> quicksort(z0)
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            part(z0,z1) -> app(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
            partGt(z0,Cons(z1,z2)) -> partGt[Ite][True][Ite](>(z1,z0),z0,Cons(z1,z2))
            partGt(z0,Nil()) -> Nil()
            partGt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partGt(z0,z2)
            partGt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partGt(z0,z2))
            partLt(z0,Cons(z1,z2)) -> partLt[Ite][True][Ite](<(z1,z0),z0,Cons(z1,z2))
            partLt(z0,Nil()) -> Nil()
            partLt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partLt(z0,z2)
            partLt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partLt(z0,z2))
            quicksort(Cons(z0,Cons(z1,z2))) -> part(z0,Cons(z1,z2))
            quicksort(Cons(z0,Nil())) -> Cons(z0,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,<'/2,>/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/2,PARTGT/2,PARTGT[ITE][TRUE][ITE]/3,PARTLT/2
            ,PARTLT[ITE][TRUE][ITE]/3,QUICKSORT/1,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3
            ,partLt/2,partLt[Ite][True][Ite]/3,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/1,c11/0
            ,c12/0,c13/2,c14/0,c15/2,c16/0,c17/1,c18/0,c19/0,c2/0,c20/0,c21/3,c22/3,c23/1,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1
            ,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PARTGT
            ,PARTGT[ITE][TRUE][ITE],PARTLT,PARTLT[ITE][TRUE][ITE],QUICKSORT,app,goal,notEmpty,part,partGt
            ,partGt[Ite][True][Ite],partLt,partLt[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(Cons(z0,z1),z2) -> c17(APP(z1,z2))
            APP(Nil(),z0) -> c18()
            GOAL(z0) -> c23(QUICKSORT(z0))
            NOTEMPTY(Cons(z0,z1)) -> c19()
            NOTEMPTY(Nil()) -> c20()
            PART(z0,z1) -> c21(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partLt(z0,z1))
                              ,PARTLT(z0,z1))
            PART(z0,z1) -> c22(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partGt(z0,z1))
                              ,PARTGT(z0,z1))
            PARTGT(z0,Cons(z1,z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1,z0),z0,Cons(z1,z2)),>'(z1,z0))
            PARTGT(z0,Nil()) -> c16()
            PARTLT(z0,Cons(z1,z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1,z0),z0,Cons(z1,z2)),<'(z1,z0))
            PARTLT(z0,Nil()) -> c14()
            QUICKSORT(Cons(z0,Cons(z1,z2))) -> c10(PART(z0,Cons(z1,z2)))
            QUICKSORT(Cons(z0,Nil())) -> c11()
            QUICKSORT(Nil()) -> c12()
        - Weak TRS:
            <(z0,0()) -> False()
            <(0(),S(z0)) -> True()
            <(S(z0),S(z1)) -> <(z0,z1)
            <'(z0,0()) -> c2()
            <'(0(),S(z0)) -> c1()
            <'(S(z0),S(z1)) -> c(<'(z0,z1))
            >(0(),z0) -> False()
            >(S(z0),0()) -> True()
            >(S(z0),S(z1)) -> >(z0,z1)
            >'(0(),z0) -> c4()
            >'(S(z0),0()) -> c5()
            >'(S(z0),S(z1)) -> c3(>'(z0,z1))
            PARTGT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c9(PARTGT(z0,z2))
            PARTGT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c8(PARTGT(z0,z2))
            PARTLT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c7(PARTLT(z0,z2))
            PARTLT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c6(PARTLT(z0,z2))
            app(Cons(z0,z1),z2) -> Cons(z0,app(z1,z2))
            app(Nil(),z0) -> z0
            goal(z0) -> quicksort(z0)
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            part(z0,z1) -> app(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
            partGt(z0,Cons(z1,z2)) -> partGt[Ite][True][Ite](>(z1,z0),z0,Cons(z1,z2))
            partGt(z0,Nil()) -> Nil()
            partGt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partGt(z0,z2)
            partGt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partGt(z0,z2))
            partLt(z0,Cons(z1,z2)) -> partLt[Ite][True][Ite](<(z1,z0),z0,Cons(z1,z2))
            partLt(z0,Nil()) -> Nil()
            partLt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partLt(z0,z2)
            partLt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partLt(z0,z2))
            quicksort(Cons(z0,Cons(z1,z2))) -> part(z0,Cons(z1,z2))
            quicksort(Cons(z0,Nil())) -> Cons(z0,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,<'/2,>/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/2,PARTGT/2,PARTGT[ITE][TRUE][ITE]/3,PARTLT/2
            ,PARTLT[ITE][TRUE][ITE]/3,QUICKSORT/1,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3
            ,partLt/2,partLt[Ite][True][Ite]/3,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/1,c11/0
            ,c12/0,c13/2,c14/0,c15/2,c16/0,c17/1,c18/0,c19/0,c2/0,c20/0,c21/3,c22/3,c23/1,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1
            ,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PARTGT
            ,PARTGT[ITE][TRUE][ITE],PARTLT,PARTLT[ITE][TRUE][ITE],QUICKSORT,app,goal,notEmpty,part,partGt
            ,partGt[Ite][True][Ite],partLt,partLt[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(Cons(z0,z1),z2) -> c17(APP(z1,z2))
            APP(Nil(),z0) -> c18()
            GOAL(z0) -> c23(QUICKSORT(z0))
            NOTEMPTY(Cons(z0,z1)) -> c19()
            NOTEMPTY(Nil()) -> c20()
            PART(z0,z1) -> c21(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partLt(z0,z1))
                              ,PARTLT(z0,z1))
            PART(z0,z1) -> c22(APP(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
                              ,QUICKSORT(partGt(z0,z1))
                              ,PARTGT(z0,z1))
            PARTGT(z0,Cons(z1,z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1,z0),z0,Cons(z1,z2)),>'(z1,z0))
            PARTGT(z0,Nil()) -> c16()
            PARTLT(z0,Cons(z1,z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1,z0),z0,Cons(z1,z2)),<'(z1,z0))
            PARTLT(z0,Nil()) -> c14()
            QUICKSORT(Cons(z0,Cons(z1,z2))) -> c10(PART(z0,Cons(z1,z2)))
            QUICKSORT(Cons(z0,Nil())) -> c11()
            QUICKSORT(Nil()) -> c12()
        - Weak TRS:
            <(z0,0()) -> False()
            <(0(),S(z0)) -> True()
            <(S(z0),S(z1)) -> <(z0,z1)
            <'(z0,0()) -> c2()
            <'(0(),S(z0)) -> c1()
            <'(S(z0),S(z1)) -> c(<'(z0,z1))
            >(0(),z0) -> False()
            >(S(z0),0()) -> True()
            >(S(z0),S(z1)) -> >(z0,z1)
            >'(0(),z0) -> c4()
            >'(S(z0),0()) -> c5()
            >'(S(z0),S(z1)) -> c3(>'(z0,z1))
            PARTGT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c9(PARTGT(z0,z2))
            PARTGT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c8(PARTGT(z0,z2))
            PARTLT[ITE][TRUE][ITE](False(),z0,Cons(z1,z2)) -> c7(PARTLT(z0,z2))
            PARTLT[ITE][TRUE][ITE](True(),z0,Cons(z1,z2)) -> c6(PARTLT(z0,z2))
            app(Cons(z0,z1),z2) -> Cons(z0,app(z1,z2))
            app(Nil(),z0) -> z0
            goal(z0) -> quicksort(z0)
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            part(z0,z1) -> app(quicksort(partLt(z0,z1)),Cons(z0,quicksort(partGt(z0,z1))))
            partGt(z0,Cons(z1,z2)) -> partGt[Ite][True][Ite](>(z1,z0),z0,Cons(z1,z2))
            partGt(z0,Nil()) -> Nil()
            partGt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partGt(z0,z2)
            partGt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partGt(z0,z2))
            partLt(z0,Cons(z1,z2)) -> partLt[Ite][True][Ite](<(z1,z0),z0,Cons(z1,z2))
            partLt(z0,Nil()) -> Nil()
            partLt[Ite][True][Ite](False(),z0,Cons(z1,z2)) -> partLt(z0,z2)
            partLt[Ite][True][Ite](True(),z0,Cons(z1,z2)) -> Cons(z1,partLt(z0,z2))
            quicksort(Cons(z0,Cons(z1,z2))) -> part(z0,Cons(z1,z2))
            quicksort(Cons(z0,Nil())) -> Cons(z0,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,<'/2,>/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/2,PARTGT/2,PARTGT[ITE][TRUE][ITE]/3,PARTLT/2
            ,PARTLT[ITE][TRUE][ITE]/3,QUICKSORT/1,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3
            ,partLt/2,partLt[Ite][True][Ite]/3,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/1,c11/0
            ,c12/0,c13/2,c14/0,c15/2,c16/0,c17/1,c18/0,c19/0,c2/0,c20/0,c21/3,c22/3,c23/1,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1
            ,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PARTGT
            ,PARTGT[ITE][TRUE][ITE],PARTLT,PARTLT[ITE][TRUE][ITE],QUICKSORT,app,goal,notEmpty,part,partGt
            ,partGt[Ite][True][Ite],partLt,partLt[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          APP(y,z){y -> Cons(x,y)} =
            APP(Cons(x,y),z) ->^+ c17(APP(y,z))
              = C[APP(y,z) = APP(y,z){}]

WORST_CASE(Omega(n^1),?)