tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(Cons(z0,z1),z2) -> c14(APP(z1,z2)) APP(Nil(),z0) -> c15() GOAL(z0) -> c18(QUICKSORT(z0)) NOTEMPTY(Cons(z0,z1)) -> c16() NOTEMPTY(Nil()) -> c17() 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)) 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() - 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)) PART[ITE][TRUE][ITE](False(),z0,Cons(z1,z2),z3,z4) -> c7(<'(z0,z1)) PART[ITE][TRUE][ITE](True(),z0,Cons(z1,z2),z3,z4) -> c6(PART(z0,z2,Cons(z1,z3),z4)) 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,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)) 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) part[Ite][True][Ite](True(),z0,Cons(z1,z2),z3,z4) -> part(z0,z2,Cons(z1,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() - Signature: {/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/4,PART[ITE][TRUE][ITE]/5,QUICKSORT/1,app/2,goal/1,notEmpty/1 ,part/4,part[Ite][True][Ite]/5,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/2 ,c12/2,c13/2,c14/1,c15/0,c16/0,c17/0,c18/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1,c9/0 ,part[Ite][True][Ite][False][Ite]/5} - Obligation: innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PART[ITE][TRUE][ITE] ,QUICKSORT,app,goal,notEmpty,part,part[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True ,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,part[Ite][True][Ite][False][Ite]} + 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) -> c14(APP(z1,z2)) APP(Nil(),z0) -> c15() GOAL(z0) -> c18(QUICKSORT(z0)) NOTEMPTY(Cons(z0,z1)) -> c16() NOTEMPTY(Nil()) -> c17() 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)) 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() - 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)) PART[ITE][TRUE][ITE](False(),z0,Cons(z1,z2),z3,z4) -> c7(<'(z0,z1)) PART[ITE][TRUE][ITE](True(),z0,Cons(z1,z2),z3,z4) -> c6(PART(z0,z2,Cons(z1,z3),z4)) 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,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)) 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) part[Ite][True][Ite](True(),z0,Cons(z1,z2),z3,z4) -> part(z0,z2,Cons(z1,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() - Signature: {/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/4,PART[ITE][TRUE][ITE]/5,QUICKSORT/1,app/2,goal/1,notEmpty/1 ,part/4,part[Ite][True][Ite]/5,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/2 ,c12/2,c13/2,c14/1,c15/0,c16/0,c17/0,c18/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1,c9/0 ,part[Ite][True][Ite][False][Ite]/5} - Obligation: innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PART[ITE][TRUE][ITE] ,QUICKSORT,app,goal,notEmpty,part,part[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True ,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,part[Ite][True][Ite][False][Ite]} + 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) -> c14(APP(z1,z2)) APP(Nil(),z0) -> c15() GOAL(z0) -> c18(QUICKSORT(z0)) NOTEMPTY(Cons(z0,z1)) -> c16() NOTEMPTY(Nil()) -> c17() 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)) 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() - 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)) PART[ITE][TRUE][ITE](False(),z0,Cons(z1,z2),z3,z4) -> c7(<'(z0,z1)) PART[ITE][TRUE][ITE](True(),z0,Cons(z1,z2),z3,z4) -> c6(PART(z0,z2,Cons(z1,z3),z4)) 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,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)) 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) part[Ite][True][Ite](True(),z0,Cons(z1,z2),z3,z4) -> part(z0,z2,Cons(z1,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() - Signature: {/2,>'/2,APP/2,GOAL/1,NOTEMPTY/1,PART/4,PART[ITE][TRUE][ITE]/5,QUICKSORT/1,app/2,goal/1,notEmpty/1 ,part/4,part[Ite][True][Ite]/5,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/2 ,c12/2,c13/2,c14/1,c15/0,c16/0,c17/0,c18/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/1,c8/1,c9/0 ,part[Ite][True][Ite][False][Ite]/5} - Obligation: innermost runtime complexity wrt. defined symbols {<,<',>,>',APP,GOAL,NOTEMPTY,PART,PART[ITE][TRUE][ITE] ,QUICKSORT,app,goal,notEmpty,part,part[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True ,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,part[Ite][True][Ite][False][Ite]} + 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) ->^+ c14(APP(y,z)) = C[APP(y,z) = APP(y,z){}] WORST_CASE(Omega(n^1),?)