MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys goal(xs) -> quicksort(xs) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) - Signature: {/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {<,>,app,goal,notEmpty,part,partGt,partGt[Ite][True][Ite] ,partLt,partLt[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) app#(Nil(),ys) -> c_2() goal#(xs) -> c_3(quicksort#(xs)) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) quicksort#(Cons(x,Nil())) -> c_12() quicksort#(Nil()) -> c_13() Weak DPs <#(x,0()) -> c_14() <#(0(),S(y)) -> c_15() <#(S(x),S(y)) -> c_16(<#(x,y)) >#(0(),y) -> c_17() >#(S(x),0()) -> c_18() >#(S(x),S(y)) -> c_19(>#(x,y)) partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) app#(Nil(),ys) -> c_2() goal#(xs) -> c_3(quicksort#(xs)) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) quicksort#(Cons(x,Nil())) -> c_12() quicksort#(Nil()) -> c_13() - Weak DPs: <#(x,0()) -> c_14() <#(0(),S(y)) -> c_15() <#(S(x),S(y)) -> c_16(<#(x,y)) >#(0(),y) -> c_17() >#(S(x),0()) -> c_18() >#(S(x),S(y)) -> c_19(>#(x,y)) partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys goal(xs) -> quicksort(xs) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() <#(x,0()) -> c_14() <#(0(),S(y)) -> c_15() <#(S(x),S(y)) -> c_16(<#(x,y)) >#(0(),y) -> c_17() >#(S(x),0()) -> c_18() >#(S(x),S(y)) -> c_19(>#(x,y)) app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) app#(Nil(),ys) -> c_2() goal#(xs) -> c_3(quicksort#(xs)) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) quicksort#(Cons(x,Nil())) -> c_12() quicksort#(Nil()) -> c_13() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) app#(Nil(),ys) -> c_2() goal#(xs) -> c_3(quicksort#(xs)) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) quicksort#(Cons(x,Nil())) -> c_12() quicksort#(Nil()) -> c_13() - Weak DPs: <#(x,0()) -> c_14() <#(0(),S(y)) -> c_15() <#(S(x),S(y)) -> c_16(<#(x,y)) >#(0(),y) -> c_17() >#(S(x),0()) -> c_18() >#(S(x),S(y)) -> c_19(>#(x,y)) partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,12,13} by application of Pre({2,4,5,12,13}) = {1,3,6}. Here rules are labelled as follows: 1: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) 2: app#(Nil(),ys) -> c_2() 3: goal#(xs) -> c_3(quicksort#(xs)) 4: notEmpty#(Cons(x,xs)) -> c_4() 5: notEmpty#(Nil()) -> c_5() 6: part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) 7: partGt#(x,Nil()) -> c_7() 8: partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) 9: partLt#(x,Nil()) -> c_9() 10: partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) 11: quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) 12: quicksort#(Cons(x,Nil())) -> c_12() 13: quicksort#(Nil()) -> c_13() 14: <#(x,0()) -> c_14() 15: <#(0(),S(y)) -> c_15() 16: <#(S(x),S(y)) -> c_16(<#(x,y)) 17: >#(0(),y) -> c_17() 18: >#(S(x),0()) -> c_18() 19: >#(S(x),S(y)) -> c_19(>#(x,y)) 20: partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) 21: partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) 22: partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) 23: partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) goal#(xs) -> c_3(quicksort#(xs)) part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) - Weak DPs: <#(x,0()) -> c_14() <#(0(),S(y)) -> c_15() <#(S(x),S(y)) -> c_16(<#(x,y)) >#(0(),y) -> c_17() >#(S(x),0()) -> c_18() >#(S(x),S(y)) -> c_19(>#(x,y)) app#(Nil(),ys) -> c_2() notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) quicksort#(Cons(x,Nil())) -> c_12() quicksort#(Nil()) -> c_13() - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) -->_1 app#(Nil(),ys) -> c_2():15 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 2:S:goal#(xs) -> c_3(quicksort#(xs)) -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_1 quicksort#(Nil()) -> c_13():23 -->_1 quicksort#(Cons(x,Nil())) -> c_12():22 3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_4 quicksort#(Nil()) -> c_13():23 -->_2 quicksort#(Nil()) -> c_13():23 -->_4 quicksort#(Cons(x,Nil())) -> c_12():22 -->_2 quicksort#(Cons(x,Nil())) -> c_12():22 -->_1 app#(Nil(),ys) -> c_2():15 -->_3 partLt#(x,Nil()) -> c_9():6 -->_5 partGt#(x,Nil()) -> c_7():4 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 4:S:partGt#(x,Nil()) -> c_7() 5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):19 -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):18 -->_2 >#(S(x),S(y)) -> c_19(>#(x,y)):14 -->_2 >#(S(x),0()) -> c_18():13 -->_2 >#(0(),y) -> c_17():12 6:S:partLt#(x,Nil()) -> c_9() 7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):21 -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):20 -->_2 <#(S(x),S(y)) -> c_16(<#(x,y)):11 -->_2 <#(0(),S(y)) -> c_15():10 -->_2 <#(x,0()) -> c_14():9 8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)):3 9:W:<#(x,0()) -> c_14() 10:W:<#(0(),S(y)) -> c_15() 11:W:<#(S(x),S(y)) -> c_16(<#(x,y)) -->_1 <#(S(x),S(y)) -> c_16(<#(x,y)):11 -->_1 <#(0(),S(y)) -> c_15():10 -->_1 <#(x,0()) -> c_14():9 12:W:>#(0(),y) -> c_17() 13:W:>#(S(x),0()) -> c_18() 14:W:>#(S(x),S(y)) -> c_19(>#(x,y)) -->_1 >#(S(x),S(y)) -> c_19(>#(x,y)):14 -->_1 >#(S(x),0()) -> c_18():13 -->_1 >#(0(),y) -> c_17():12 15:W:app#(Nil(),ys) -> c_2() 16:W:notEmpty#(Cons(x,xs)) -> c_4() 17:W:notEmpty#(Nil()) -> c_5() 18:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_1 partGt#(x,Nil()) -> c_7():4 19:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_1 partGt#(x,Nil()) -> c_7():4 20:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_1 partLt#(x,Nil()) -> c_9():6 21:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_1 partLt#(x,Nil()) -> c_9():6 22:W:quicksort#(Cons(x,Nil())) -> c_12() 23:W:quicksort#(Nil()) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: notEmpty#(Nil()) -> c_5() 16: notEmpty#(Cons(x,xs)) -> c_4() 22: quicksort#(Cons(x,Nil())) -> c_12() 23: quicksort#(Nil()) -> c_13() 14: >#(S(x),S(y)) -> c_19(>#(x,y)) 12: >#(0(),y) -> c_17() 13: >#(S(x),0()) -> c_18() 11: <#(S(x),S(y)) -> c_16(<#(x,y)) 9: <#(x,0()) -> c_14() 10: <#(0(),S(y)) -> c_15() 15: app#(Nil(),ys) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) goal#(xs) -> c_3(quicksort#(xs)) part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) - Weak DPs: partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 2:S:goal#(xs) -> c_3(quicksort#(xs)) -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_3 partLt#(x,Nil()) -> c_9():6 -->_5 partGt#(x,Nil()) -> c_7():4 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 4:S:partGt#(x,Nil()) -> c_7() 5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')) -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):19 -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):18 6:S:partLt#(x,Nil()) -> c_9() 7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')) -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):21 -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):20 8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)):3 18:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_1 partGt#(x,Nil()) -> c_7():4 19:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5 -->_1 partGt#(x,Nil()) -> c_7():4 20:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_1 partLt#(x,Nil()) -> c_9():6 21:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7 -->_1 partLt#(x,Nil()) -> c_9():6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))) partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) goal#(xs) -> c_3(quicksort#(xs)) part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) - Weak DPs: partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 2:S:goal#(xs) -> c_3(quicksort#(xs)) -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8 -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7 -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5 -->_3 partLt#(x,Nil()) -> c_9():6 -->_5 partGt#(x,Nil()) -> c_7():4 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1 4:S:partGt#(x,Nil()) -> c_7() 5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))) -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):10 -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):9 6:S:partLt#(x,Nil()) -> c_9() 7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))) -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):12 -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):11 8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)):3 9:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5 -->_1 partGt#(x,Nil()) -> c_7():4 10:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5 -->_1 partGt#(x,Nil()) -> c_7():4 11:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7 -->_1 partLt#(x,Nil()) -> c_9():6 12:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7 -->_1 partLt#(x,Nil()) -> c_9():6 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(2,goal#(xs) -> c_3(quicksort#(xs)))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)) part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) ,quicksort#(partLt(x,xs)) ,partLt#(x,xs) ,quicksort#(partGt(x,xs)) ,partGt#(x,xs)) partGt#(x,Nil()) -> c_7() partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))) partLt#(x,Nil()) -> c_9() partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))) quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))) - Weak DPs: partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)) partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)) partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)) partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) >(0(),y) -> False() >(S(x),0()) -> True() >(S(x),S(y)) -> >(x,y) app(Cons(x,xs),ys) -> Cons(x,app(xs,ys)) app(Nil(),ys) -> ys part(x,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs)))) partGt(x,Nil()) -> Nil() partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs)) partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs) partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs)) partLt(x,Nil()) -> Nil() partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs)) partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs) partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs)) quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs)) quicksort(Cons(x,Nil())) -> Cons(x,Nil()) quicksort(Nil()) -> Nil() - Signature: {/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,<#/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} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/5,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1 ,c_21/1,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt# ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S ,True} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE