*** 1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
        app(Nil(),ys) -> ys
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        part(x,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Weak DP Rules:
        
      Weak TRS 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)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {<,>,app,notEmpty,part,part[False][Ite],part[Ite],qs,quicksort}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        app#(Nil(),ys) -> c_2()
        notEmpty#(Cons(x,xs)) -> c_3()
        notEmpty#(Nil()) -> c_4()
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        quicksort#(Cons(x,Nil())) -> c_9()
        quicksort#(Nil()) -> c_10()
      Weak DPs
        <#(x,0()) -> c_11()
        <#(0(),S(y)) -> c_12()
        <#(S(x),S(y)) -> c_13(<#(x,y))
        >#(0(),y) -> c_14()
        >#(S(x),0()) -> c_15()
        >#(S(x),S(y)) -> c_16(>#(x,y))
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        app#(Nil(),ys) -> c_2()
        notEmpty#(Cons(x,xs)) -> c_3()
        notEmpty#(Nil()) -> c_4()
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        quicksort#(Cons(x,Nil())) -> c_9()
        quicksort#(Nil()) -> c_10()
      Strict TRS Rules:
        
      Weak DP Rules:
        <#(x,0()) -> c_11()
        <#(0(),S(y)) -> c_12()
        <#(S(x),S(y)) -> c_13(<#(x,y))
        >#(0(),y) -> c_14()
        >#(S(x),0()) -> c_15()
        >#(S(x),S(y)) -> c_16(>#(x,y))
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
      Weak TRS 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
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        part(x,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/2,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/2,c_20/1}
      Obligation:
        Innermost
        basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      UsableRules
    Proof:
      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,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
        <#(x,0()) -> c_11()
        <#(0(),S(y)) -> c_12()
        <#(S(x),S(y)) -> c_13(<#(x,y))
        >#(0(),y) -> c_14()
        >#(S(x),0()) -> c_15()
        >#(S(x),S(y)) -> c_16(>#(x,y))
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        app#(Nil(),ys) -> c_2()
        notEmpty#(Cons(x,xs)) -> c_3()
        notEmpty#(Nil()) -> c_4()
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        quicksort#(Cons(x,Nil())) -> c_9()
        quicksort#(Nil()) -> c_10()
*** 1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        app#(Nil(),ys) -> c_2()
        notEmpty#(Cons(x,xs)) -> c_3()
        notEmpty#(Nil()) -> c_4()
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        quicksort#(Cons(x,Nil())) -> c_9()
        quicksort#(Nil()) -> c_10()
      Strict TRS Rules:
        
      Weak DP Rules:
        <#(x,0()) -> c_11()
        <#(0(),S(y)) -> c_12()
        <#(S(x),S(y)) -> c_13(<#(x,y))
        >#(0(),y) -> c_14()
        >#(S(x),0()) -> c_15()
        >#(S(x),S(y)) -> c_16(>#(x,y))
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
      Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/2,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/2,c_20/1}
      Obligation:
        Innermost
        basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {2,3,4,9,10}
      by application of
        Pre({2,3,4,9,10}) = {1,5,7}.
      Here rules are labelled as follows:
        1:  app#(Cons(x,xs),ys) ->                                   
              c_1(app#(xs,ys))                                       
        2:  app#(Nil(),ys) -> c_2()                                  
        3:  notEmpty#(Cons(x,xs)) -> c_3()                           
        4:  notEmpty#(Nil()) -> c_4()                                
        5:  part#(x,Nil(),xs1,xs2) ->                                
              c_5(app#(xs1,xs2))                                     
        6:  part#(x',Cons(x,xs),xs1,xs2) ->                          
              c_6(part[Ite]#(>(x',x)                                 
                            ,x'                                      
                            ,Cons(x,xs)                              
                            ,xs1                                     
                            ,xs2)                                    
                 ,>#(x',x))                                          
        7:  qs#(x',Cons(x,xs)) ->                                    
              c_7(app#(Cons(x,Nil())                                 
                      ,Cons(x',quicksort(xs)))                       
                 ,quicksort#(xs))                                    
        8:  quicksort#(Cons(x                                        
                           ,Cons(x',xs))) -> c_8(qs#(x               
                                                    ,part(x          
                                                         ,Cons(x',xs)
                                                         ,Nil()      
                                                         ,Nil()))    
                                                ,part#(x             
                                                      ,Cons(x',xs)   
                                                      ,Nil()         
                                                      ,Nil()))       
        9:  quicksort#(Cons(x,Nil())) ->                             
              c_9()                                                  
        10: quicksort#(Nil()) -> c_10()                              
        11: <#(x,0()) -> c_11()                                      
        12: <#(0(),S(y)) -> c_12()                                   
        13: <#(S(x),S(y)) -> c_13(<#(x,y))                           
        14: >#(0(),y) -> c_14()                                      
        15: >#(S(x),0()) -> c_15()                                   
        16: >#(S(x),S(y)) -> c_16(>#(x,y))                           
        17: part[False][Ite]#(False()                                
                             ,x'                                     
                             ,Cons(x,xs)                             
                             ,xs1                                    
                             ,xs2) -> c_17(part#(x'                  
                                                ,xs                  
                                                ,xs1                 
                                                ,xs2))               
        18: part[False][Ite]#(True()                                 
                             ,x'                                     
                             ,Cons(x,xs)                             
                             ,xs1                                    
                             ,xs2) -> c_18(part#(x'                  
                                                ,xs                  
                                                ,xs1                 
                                                ,Cons(x,xs2)))       
        19: part[Ite]#(False()                                       
                      ,x'                                            
                      ,Cons(x,xs)                                    
                      ,xs1                                           
                      ,xs2) ->                                       
              c_19(part[False][Ite]#(<(x',x)                         
                                    ,x'                              
                                    ,Cons(x,xs)                      
                                    ,xs1                             
                                    ,xs2)                            
                  ,<#(x',x))                                         
        20: part[Ite]#(True()                                        
                      ,x'                                            
                      ,Cons(x,xs)                                    
                      ,xs1                                           
                      ,xs2) -> c_20(part#(x'                         
                                         ,xs                         
                                         ,Cons(x,xs1)                
                                         ,xs2))                      
*** 1.1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
      Strict TRS Rules:
        
      Weak DP Rules:
        <#(x,0()) -> c_11()
        <#(0(),S(y)) -> c_12()
        <#(S(x),S(y)) -> c_13(<#(x,y))
        >#(0(),y) -> c_14()
        >#(S(x),0()) -> c_15()
        >#(S(x),S(y)) -> c_16(>#(x,y))
        app#(Nil(),ys) -> c_2()
        notEmpty#(Cons(x,xs)) -> c_3()
        notEmpty#(Nil()) -> c_4()
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        quicksort#(Cons(x,Nil())) -> c_9()
        quicksort#(Nil()) -> c_10()
      Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/2,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/2,c_20/1}
      Obligation:
        Innermost
        basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
           -->_1 app#(Nil(),ys) -> c_2():12
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        2:S:part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
           -->_1 app#(Nil(),ys) -> c_2():12
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        3:S:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
           -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):18
           -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x)):17
           -->_2 >#(S(x),S(y)) -> c_16(>#(x,y)):11
           -->_2 >#(S(x),0()) -> c_15():10
           -->_2 >#(0(),y) -> c_14():9
        
        4:S:qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
           -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):5
           -->_2 quicksort#(Nil()) -> c_10():20
           -->_2 quicksort#(Cons(x,Nil())) -> c_9():19
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        5:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
           -->_1 qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs)):4
           -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
        
        6:W:<#(x,0()) -> c_11()
           
        
        7:W:<#(0(),S(y)) -> c_12()
           
        
        8:W:<#(S(x),S(y)) -> c_13(<#(x,y))
           -->_1 <#(S(x),S(y)) -> c_13(<#(x,y)):8
           -->_1 <#(0(),S(y)) -> c_12():7
           -->_1 <#(x,0()) -> c_11():6
        
        9:W:>#(0(),y) -> c_14()
           
        
        10:W:>#(S(x),0()) -> c_15()
           
        
        11:W:>#(S(x),S(y)) -> c_16(>#(x,y))
           -->_1 >#(S(x),S(y)) -> c_16(>#(x,y)):11
           -->_1 >#(S(x),0()) -> c_15():10
           -->_1 >#(0(),y) -> c_14():9
        
        12:W:app#(Nil(),ys) -> c_2()
           
        
        13:W:notEmpty#(Cons(x,xs)) -> c_3()
           
        
        14:W:notEmpty#(Nil()) -> c_4()
           
        
        15:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
        16:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
        17:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
           -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):16
           -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):15
           -->_2 <#(S(x),S(y)) -> c_13(<#(x,y)):8
           -->_2 <#(0(),S(y)) -> c_12():7
           -->_2 <#(x,0()) -> c_11():6
        
        18:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
        19:W:quicksort#(Cons(x,Nil())) -> c_9()
           
        
        20:W:quicksort#(Nil()) -> c_10()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        14: notEmpty#(Nil()) -> c_4()     
        13: notEmpty#(Cons(x,xs)) -> c_3()
        19: quicksort#(Cons(x,Nil())) ->  
              c_9()                       
        20: quicksort#(Nil()) -> c_10()   
        11: >#(S(x),S(y)) -> c_16(>#(x,y))
        9:  >#(0(),y) -> c_14()           
        10: >#(S(x),0()) -> c_15()        
        8:  <#(S(x),S(y)) -> c_13(<#(x,y))
        6:  <#(x,0()) -> c_11()           
        7:  <#(0(),S(y)) -> c_12()        
        12: app#(Nil(),ys) -> c_2()       
*** 1.1.1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
      Strict TRS Rules:
        
      Weak DP Rules:
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
      Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/2,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/2,c_20/1}
      Obligation:
        Innermost
        basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      SimplifyRHS
    Proof:
      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:part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        3:S:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
           -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):18
           -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x)):17
        
        4:S:qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
           -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):5
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        5:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
           -->_1 qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs)):4
           -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
        
        15:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
        16:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
        17:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2),<#(x',x))
           -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):16
           -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):15
        
        18:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x)):3
           -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
        
      Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
        part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
        qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
        quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
      Strict TRS Rules:
        
      Weak DP Rules:
        part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
        part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
        part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
        part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
      Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
        part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
        part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
        part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
        part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
        part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
        quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
        quicksort(Cons(x,Nil())) -> Cons(x,Nil())
        quicksort(Nil()) -> Nil()
      Signature:
        {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
      Obligation:
        Innermost
        basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    Proof:
      We analyse the complexity of following sub-problems (R) and (S).
      Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
      
      Problem (R)
        Strict DP Rules:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        Strict TRS Rules:
          
        Weak DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      
      Problem (S)
        Strict DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Strict TRS Rules:
          
        Weak DP Rules:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
  *** 1.1.1.1.1.1.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
        Strict TRS Rules:
          
        Weak DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
      Proof:
        We decompose the input problem according to the dependency graph into the upper component
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        and a lower component
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Further, following extension rules are added to the lower component.
          qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
          qs#(x',Cons(x,xs)) -> quicksort#(xs)
          quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
          quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
    *** 1.1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
            quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: qs#(x',Cons(x,xs)) ->                                    
                 c_7(app#(Cons(x,Nil())                                 
                         ,Cons(x',quicksort(xs)))                       
                    ,quicksort#(xs))                                    
            2: quicksort#(Cons(x                                        
                              ,Cons(x',xs))) -> c_8(qs#(x               
                                                       ,part(x          
                                                            ,Cons(x',xs)
                                                            ,Nil()      
                                                            ,Nil()))    
                                                   ,part#(x             
                                                         ,Cons(x',xs)   
                                                         ,Nil()         
                                                         ,Nil()))       
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_7) = {1,2},
              uargs(c_8) = {1}
            
            Following symbols are considered usable:
              {app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
            TcT has computed the following interpretation:
                              p(0) = [1]                           
                              p(<) = [2] x1 + [0]                  
                              p(>) = [0]                           
                           p(Cons) = [1] x2 + [1]                  
                          p(False) = [0]                           
                            p(Nil) = [0]                           
                              p(S) = [1] x1 + [0]                  
                           p(True) = [0]                           
                            p(app) = [1] x1 + [1] x2 + [0]         
                       p(notEmpty) = [2]                           
                           p(part) = [1] x2 + [1] x3 + [1] x4 + [0]
               p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                      p(part[Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                             p(qs) = [5] x1 + [7]                  
                      p(quicksort) = [4] x1 + [0]                  
                             p(<#) = [1]                           
                             p(>#) = [1] x2 + [1]                  
                           p(app#) = [0]                           
                      p(notEmpty#) = [1] x1 + [1]                  
                          p(part#) = [1] x3 + [2] x4 + [1]         
              p(part[False][Ite]#) = [1] x3 + [4] x4 + [1] x5 + [1]
                     p(part[Ite]#) = [4] x1 + [1] x4 + [4] x5 + [4]
                            p(qs#) = [2] x2 + [0]                  
                     p(quicksort#) = [2] x1 + [1]                  
                            p(c_1) = [1]                           
                            p(c_2) = [4]                           
                            p(c_3) = [0]                           
                            p(c_4) = [1]                           
                            p(c_5) = [0]                           
                            p(c_6) = [0]                           
                            p(c_7) = [2] x1 + [1] x2 + [0]         
                            p(c_8) = [1] x1 + [2] x2 + [0]         
                            p(c_9) = [0]                           
                           p(c_10) = [0]                           
                           p(c_11) = [1]                           
                           p(c_12) = [0]                           
                           p(c_13) = [4] x1 + [4]                  
                           p(c_14) = [0]                           
                           p(c_15) = [1]                           
                           p(c_16) = [0]                           
                           p(c_17) = [0]                           
                           p(c_18) = [1]                           
                           p(c_19) = [4] x1 + [1]                  
                           p(c_20) = [4] x1 + [0]                  
            
            Following rules are strictly oriented:
                         qs#(x',Cons(x,xs)) = [2] xs + [2]                    
                                            > [2] xs + [1]                    
                                            = c_7(app#(Cons(x,Nil())          
                                                      ,Cons(x',quicksort(xs)))
                                                 ,quicksort#(xs))             
            
            quicksort#(Cons(x,Cons(x',xs))) = [2] xs + [5]                    
                                            > [2] xs + [4]                    
                                            = c_8(qs#(x                       
                                                     ,part(x                  
                                                          ,Cons(x',xs)        
                                                          ,Nil()              
                                                          ,Nil()))            
                                                 ,part#(x                     
                                                       ,Cons(x',xs)           
                                                       ,Nil()                 
                                                       ,Nil()))               
            
            
            Following rules are (at-least) weakly oriented:
                     app(Cons(x,xs),ys) =  [1] xs + [1] ys + [1]           
                                        >= [1] xs + [1] ys + [1]           
                                        =  Cons(x,app(xs,ys))              
            
                          app(Nil(),ys) =  [1] ys + [0]                    
                                        >= [1] ys + [0]                    
                                        =  ys                              
            
                  part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [0]         
                                        >= [1] xs1 + [1] xs2 + [0]         
                                        =  app(xs1,xs2)                    
            
            part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [1]
                                        >= [1] xs + [1] xs1 + [1] xs2 + [1]
                                        =  part[Ite](>(x',x)               
                                                    ,x'                    
                                                    ,Cons(x,xs)            
                                                    ,xs1                   
                                                    ,xs2)                  
            
               part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1]
                                    ,x'                                    
                            ,Cons(x,xs)                                    
                                   ,xs1                                    
                                  ,xs2)                                    
                                        >= [1] xs + [1] xs1 + [1] xs2 + [0]
                                        =  part(x',xs,xs1,xs2)             
            
                part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1]
                                    ,x'                                    
                            ,Cons(x,xs)                                    
                                   ,xs1                                    
                                  ,xs2)                                    
                                        >= [1] xs + [1] xs1 + [1] xs2 + [1]
                                        =  part(x',xs,xs1,Cons(x,xs2))     
            
                      part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1]
                                    ,x'                                    
                            ,Cons(x,xs)                                    
                                   ,xs1                                    
                                  ,xs2)                                    
                                        >= [1] xs + [1] xs1 + [1] xs2 + [1]
                                        =  part[False][Ite](<(x',x)        
                                                           ,x'             
                                                           ,Cons(x,xs)     
                                                           ,xs1            
                                                           ,xs2)           
            
                       part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1]
                                    ,x'                                    
                            ,Cons(x,xs)                                    
                                   ,xs1                                    
                                  ,xs2)                                    
                                        >= [1] xs + [1] xs1 + [1] xs2 + [1]
                                        =  part(x',xs,Cons(x,xs1),xs2)     
            
      *** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
                 -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):2
              
              2:W:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                 -->_1 qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs)):1
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              1: qs#(x',Cons(x,xs)) ->                                    
                   c_7(app#(Cons(x,Nil())                                 
                           ,Cons(x',quicksort(xs)))                       
                      ,quicksort#(xs))                                    
              2: quicksort#(Cons(x                                        
                                ,Cons(x',xs))) -> c_8(qs#(x               
                                                         ,part(x          
                                                              ,Cons(x',xs)
                                                              ,Nil()      
                                                              ,Nil()))    
                                                     ,part#(x             
                                                           ,Cons(x',xs)   
                                                           ,Nil()         
                                                           ,Nil()))       
      *** 1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
    *** 1.1.1.1.1.1.1.2 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          Strict TRS Rules:
            
          Weak DP Rules:
            part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
            qs#(x',Cons(x,xs)) -> quicksort#(xs)
            quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
            quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
            quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: app#(Cons(x,xs),ys) ->
                 c_1(app#(xs,ys))    
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
              qs#(x',Cons(x,xs)) -> quicksort#(xs)
              quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
              quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_1) = {1},
              uargs(c_5) = {1},
              uargs(c_6) = {1},
              uargs(c_17) = {1},
              uargs(c_18) = {1},
              uargs(c_19) = {1},
              uargs(c_20) = {1}
            
            Following symbols are considered usable:
              {app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
            TcT has computed the following interpretation:
                              p(0) = [0]                           
                              p(<) = [0]                           
                              p(>) = [0]                           
                           p(Cons) = [1] x2 + [2]                  
                          p(False) = [0]                           
                            p(Nil) = [0]                           
                              p(S) = [1] x1 + [0]                  
                           p(True) = [0]                           
                            p(app) = [1] x1 + [1] x2 + [0]         
                       p(notEmpty) = [1]                           
                           p(part) = [1] x2 + [1] x3 + [1] x4 + [0]
               p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                      p(part[Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                             p(qs) = [4] x2 + [4]                  
                      p(quicksort) = [1] x1 + [0]                  
                             p(<#) = [1] x1 + [1] x2 + [2]         
                             p(>#) = [4]                           
                           p(app#) = [1] x1 + [0]                  
                      p(notEmpty#) = [2] x1 + [1]                  
                          p(part#) = [1] x2 + [1] x3 + [0]         
              p(part[False][Ite]#) = [1] x3 + [1] x4 + [0]         
                     p(part[Ite]#) = [1] x3 + [1] x4 + [0]         
                            p(qs#) = [1] x2 + [2]                  
                     p(quicksort#) = [1] x1 + [0]                  
                            p(c_1) = [1] x1 + [0]                  
                            p(c_2) = [1]                           
                            p(c_3) = [0]                           
                            p(c_4) = [0]                           
                            p(c_5) = [1] x1 + [0]                  
                            p(c_6) = [1] x1 + [0]                  
                            p(c_7) = [4]                           
                            p(c_8) = [0]                           
                            p(c_9) = [0]                           
                           p(c_10) = [1]                           
                           p(c_11) = [1]                           
                           p(c_12) = [2]                           
                           p(c_13) = [1] x1 + [1]                  
                           p(c_14) = [0]                           
                           p(c_15) = [0]                           
                           p(c_16) = [4] x1 + [0]                  
                           p(c_17) = [1] x1 + [1]                  
                           p(c_18) = [1] x1 + [2]                  
                           p(c_19) = [1] x1 + [0]                  
                           p(c_20) = [1] x1 + [0]                  
            
            Following rules are strictly oriented:
            app#(Cons(x,xs),ys) = [1] xs + [2]    
                                > [1] xs + [0]    
                                = c_1(app#(xs,ys))
            
            
            Following rules are (at-least) weakly oriented:
                     part#(x,Nil(),xs1,xs2) =  [1] xs1 + [0]                    
                                            >= [1] xs1 + [0]                    
                                            =  c_5(app#(xs1,xs2))               
            
               part#(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [2]           
                                            >= [1] xs + [1] xs1 + [2]           
                                            =  c_6(part[Ite]#(>(x',x)           
                                                             ,x'                
                                                             ,Cons(x,xs)        
                                                             ,xs1               
                                                             ,xs2))             
            
                  part[False][Ite]#(False() =  [1] xs + [1] xs1 + [2]           
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1]           
                                            =  c_17(part#(x',xs,xs1,xs2))       
            
                   part[False][Ite]#(True() =  [1] xs + [1] xs1 + [2]           
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [2]           
                                            =  c_18(part#(x'                    
                                                         ,xs                    
                                                         ,xs1                   
                                                         ,Cons(x,xs2)))         
            
                         part[Ite]#(False() =  [1] xs + [1] xs1 + [2]           
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [2]           
                                            =  c_19(part[False][Ite]#(<(x',x)   
                                                                     ,x'        
                                                                     ,Cons(x,xs)
                                                                     ,xs1       
                                                                     ,xs2))     
            
                          part[Ite]#(True() =  [1] xs + [1] xs1 + [2]           
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [2]           
                                            =  c_20(part#(x'                    
                                                         ,xs                    
                                                         ,Cons(x,xs1)           
                                                         ,xs2))                 
            
                         qs#(x',Cons(x,xs)) =  [1] xs + [4]                     
                                            >= [2]                              
                                            =  app#(Cons(x,Nil())               
                                                   ,Cons(x',quicksort(xs)))     
            
                         qs#(x',Cons(x,xs)) =  [1] xs + [4]                     
                                            >= [1] xs + [0]                     
                                            =  quicksort#(xs)                   
            
            quicksort#(Cons(x,Cons(x',xs))) =  [1] xs + [4]                     
                                            >= [1] xs + [2]                     
                                            =  part#(x,Cons(x',xs),Nil(),Nil()) 
            
            quicksort#(Cons(x,Cons(x',xs))) =  [1] xs + [4]                     
                                            >= [1] xs + [4]                     
                                            =  qs#(x                            
                                                  ,part(x                       
                                                       ,Cons(x',xs)             
                                                       ,Nil()                   
                                                       ,Nil()))                 
            
                         app(Cons(x,xs),ys) =  [1] xs + [1] ys + [2]            
                                            >= [1] xs + [1] ys + [2]            
                                            =  Cons(x,app(xs,ys))               
            
                              app(Nil(),ys) =  [1] ys + [0]                     
                                            >= [1] ys + [0]                     
                                            =  ys                               
            
                      part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [0]          
                                            >= [1] xs1 + [1] xs2 + [0]          
                                            =  app(xs1,xs2)                     
            
                part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [2] 
                                            >= [1] xs + [1] xs1 + [1] xs2 + [2] 
                                            =  part[Ite](>(x',x)                
                                                        ,x'                     
                                                        ,Cons(x,xs)             
                                                        ,xs1                    
                                                        ,xs2)                   
            
                   part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [2] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [0] 
                                            =  part(x',xs,xs1,xs2)              
            
                    part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [2] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [2] 
                                            =  part(x',xs,xs1,Cons(x,xs2))      
            
                          part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [2] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [2] 
                                            =  part[False][Ite](<(x',x)         
                                                               ,x'              
                                                               ,Cons(x,xs)      
                                                               ,xs1             
                                                               ,xs2)            
            
                           part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [2] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [2] 
                                            =  part(x',xs,Cons(x,xs1),xs2)      
            
      *** 1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
              part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
              qs#(x',Cons(x,xs)) -> quicksort#(xs)
              quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
              quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
              part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
              qs#(x',Cons(x,xs)) -> quicksort#(xs)
              quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
              quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
                 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
              
              2:W:part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
                 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
              
              3:W:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):7
                 -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):6
              
              4:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
              
              5:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
              
              6:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):5
                 -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):4
              
              7:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):2
              
              8:W:qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs)))
                 -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
              
              9:W:qs#(x',Cons(x,xs)) -> quicksort#(xs)
                 -->_1 quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil())):11
                 -->_1 quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil()):10
              
              10:W:quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
              
              11:W:quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
                 -->_1 qs#(x',Cons(x,xs)) -> quicksort#(xs):9
                 -->_1 qs#(x',Cons(x,xs)) -> app#(Cons(x,Nil()),Cons(x',quicksort(xs))):8
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              9:  qs#(x',Cons(x,xs)) ->                                
                    quicksort#(xs)                                     
              11: quicksort#(Cons(x                                    
                                 ,Cons(x',xs))) -> qs#(x               
                                                      ,part(x          
                                                           ,Cons(x',xs)
                                                           ,Nil()      
                                                           ,Nil()))    
              10: quicksort#(Cons(x                                    
                                 ,Cons(x',xs))) -> part#(x             
                                                        ,Cons(x',xs)   
                                                        ,Nil()         
                                                        ,Nil())        
              8:  qs#(x',Cons(x,xs)) ->                                
                    app#(Cons(x,Nil())                                 
                        ,Cons(x',quicksort(xs)))                       
              3:  part#(x',Cons(x,xs),xs1,xs2) ->                      
                    c_6(part[Ite]#(>(x',x)                             
                                  ,x'                                  
                                  ,Cons(x,xs)                          
                                  ,xs1                                 
                                  ,xs2))                               
              7:  part[Ite]#(True()                                    
                            ,x'                                        
                            ,Cons(x,xs)                                
                            ,xs1                                       
                            ,xs2) -> c_20(part#(x'                     
                                               ,xs                     
                                               ,Cons(x,xs1)            
                                               ,xs2))                  
              5:  part[False][Ite]#(True()                             
                                   ,x'                                 
                                   ,Cons(x,xs)                         
                                   ,xs1                                
                                   ,xs2) -> c_18(part#(x'              
                                                      ,xs              
                                                      ,xs1             
                                                      ,Cons(x,xs2)))   
              6:  part[Ite]#(False()                                   
                            ,x'                                        
                            ,Cons(x,xs)                                
                            ,xs1                                       
                            ,xs2) ->                                   
                    c_19(part[False][Ite]#(<(x',x)                     
                                          ,x'                          
                                          ,Cons(x,xs)                  
                                          ,xs1                         
                                          ,xs2))                       
              4:  part[False][Ite]#(False()                            
                                   ,x'                                 
                                   ,Cons(x,xs)                         
                                   ,xs1                                
                                   ,xs2) -> c_17(part#(x'              
                                                      ,xs              
                                                      ,xs1             
                                                      ,xs2))           
              2:  part#(x,Nil(),xs1,xs2) ->                            
                    c_5(app#(xs1,xs2))                                 
              1:  app#(Cons(x,xs),ys) ->                               
                    c_1(app#(xs,ys))                                   
      *** 1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
              quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
  *** 1.1.1.1.1.1.2 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Strict TRS Rules:
          
        Weak DP Rules:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      Applied Processor:
        RemoveWeakSuffixes
      Proof:
        Consider the dependency graph
          1:S:part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):5
          
          2:S:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):9
             -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):8
          
          3:S:qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):5
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):4
          
          4:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
             -->_1 qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs)):3
             -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
          
          5:W:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):5
          
          6:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
          7:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
          8:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):7
             -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):6
          
          9:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          5: app#(Cons(x,xs),ys) ->
               c_1(app#(xs,ys))    
  *** 1.1.1.1.1.1.2.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Strict TRS Rules:
          
        Weak DP Rules:
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      Applied Processor:
        SimplifyRHS
      Proof:
        Consider the dependency graph
          1:S:part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2))
             
          
          2:S:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):9
             -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):8
          
          3:S:qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs))
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):4
          
          4:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
             -->_1 qs#(x',Cons(x,xs)) -> c_7(app#(Cons(x,Nil()),Cons(x',quicksort(xs))),quicksort#(xs)):3
             -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
          
          6:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
          7:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
          8:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):7
             -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):6
          
          9:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_5(app#(xs1,xs2)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          part#(x,Nil(),xs1,xs2) -> c_5()
          qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
  *** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5()
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Strict TRS Rules:
          
        Weak DP Rules:
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          qs(x',Cons(x,xs)) -> app(Cons(x,Nil()),Cons(x',quicksort(xs)))
          quicksort(Cons(x,Cons(x',xs))) -> qs(x,part(x,Cons(x',xs),Nil(),Nil()))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      Applied Processor:
        UsableRules
      Proof:
        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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          part#(x,Nil(),xs1,xs2) -> c_5()
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
  *** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          part#(x,Nil(),xs1,xs2) -> c_5()
          part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
        Strict TRS Rules:
          
        Weak DP Rules:
          part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
          part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
          part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
        Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
          part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
          part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        Signature:
          {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
        Obligation:
          Innermost
          basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
      Proof:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          Strict DP Rules:
            part#(x,Nil(),xs1,xs2) -> c_5()
          Strict TRS Rules:
            
          Weak DP Rules:
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        
        Problem (S)
          Strict DP Rules:
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Strict TRS Rules:
            
          Weak DP Rules:
            part#(x,Nil(),xs1,xs2) -> c_5()
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
    *** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            part#(x,Nil(),xs1,xs2) -> c_5()
          Strict TRS Rules:
            
          Weak DP Rules:
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: part#(x,Nil(),xs1,xs2) -> c_5()
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              part#(x,Nil(),xs1,xs2) -> c_5()
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_6) = {1},
              uargs(c_7) = {1},
              uargs(c_8) = {1,2},
              uargs(c_17) = {1},
              uargs(c_18) = {1},
              uargs(c_19) = {1},
              uargs(c_20) = {1}
            
            Following symbols are considered usable:
              {>,app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
            TcT has computed the following interpretation:
                              p(0) = [0]                           
                              p(<) = [0]                           
                              p(>) = [1]                           
                           p(Cons) = [1] x2 + [1]                  
                          p(False) = [1]                           
                            p(Nil) = [0]                           
                              p(S) = [1] x1 + [0]                  
                           p(True) = [1]                           
                            p(app) = [1] x1 + [1] x2 + [0]         
                       p(notEmpty) = [0]                           
                           p(part) = [1] x2 + [1] x3 + [1] x4 + [0]
               p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                      p(part[Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                             p(qs) = [1] x1 + [1] x2 + [0]         
                      p(quicksort) = [0]                           
                             p(<#) = [1] x2 + [1]                  
                             p(>#) = [1] x1 + [1]                  
                           p(app#) = [2] x2 + [0]                  
                      p(notEmpty#) = [4] x1 + [4]                  
                          p(part#) = [6]                           
              p(part[False][Ite]#) = [6]                           
                     p(part[Ite]#) = [6] x1 + [0]                  
                            p(qs#) = [5] x2 + [3]                  
                     p(quicksort#) = [5] x1 + [4]                  
                            p(c_1) = [0]                           
                            p(c_2) = [0]                           
                            p(c_3) = [0]                           
                            p(c_4) = [1]                           
                            p(c_5) = [2]                           
                            p(c_6) = [1] x1 + [0]                  
                            p(c_7) = [1] x1 + [4]                  
                            p(c_8) = [1] x1 + [1] x2 + [0]         
                            p(c_9) = [1]                           
                           p(c_10) = [4]                           
                           p(c_11) = [0]                           
                           p(c_12) = [1]                           
                           p(c_13) = [1] x1 + [1]                  
                           p(c_14) = [0]                           
                           p(c_15) = [0]                           
                           p(c_16) = [4]                           
                           p(c_17) = [1] x1 + [0]                  
                           p(c_18) = [1] x1 + [0]                  
                           p(c_19) = [1] x1 + [0]                  
                           p(c_20) = [1] x1 + [0]                  
            
            Following rules are strictly oriented:
            part#(x,Nil(),xs1,xs2) = [6]  
                                   > [2]  
                                   = c_5()
            
            
            Following rules are (at-least) weakly oriented:
               part#(x',Cons(x,xs),xs1,xs2) =  [6]                              
                                            >= [6]                              
                                            =  c_6(part[Ite]#(>(x',x)           
                                                             ,x'                
                                                             ,Cons(x,xs)        
                                                             ,xs1               
                                                             ,xs2))             
            
                  part[False][Ite]#(False() =  [6]                              
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [6]                              
                                            =  c_17(part#(x',xs,xs1,xs2))       
            
                   part[False][Ite]#(True() =  [6]                              
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [6]                              
                                            =  c_18(part#(x'                    
                                                         ,xs                    
                                                         ,xs1                   
                                                         ,Cons(x,xs2)))         
            
                         part[Ite]#(False() =  [6]                              
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [6]                              
                                            =  c_19(part[False][Ite]#(<(x',x)   
                                                                     ,x'        
                                                                     ,Cons(x,xs)
                                                                     ,xs1       
                                                                     ,xs2))     
            
                          part[Ite]#(True() =  [6]                              
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [6]                              
                                            =  c_20(part#(x'                    
                                                         ,xs                    
                                                         ,Cons(x,xs1)           
                                                         ,xs2))                 
            
                         qs#(x',Cons(x,xs)) =  [5] xs + [8]                     
                                            >= [5] xs + [8]                     
                                            =  c_7(quicksort#(xs))              
            
            quicksort#(Cons(x,Cons(x',xs))) =  [5] xs + [14]                    
                                            >= [5] xs + [14]                    
                                            =  c_8(qs#(x                        
                                                      ,part(x                   
                                                           ,Cons(x',xs)         
                                                           ,Nil()               
                                                           ,Nil()))             
                                                  ,part#(x                      
                                                        ,Cons(x',xs)            
                                                        ,Nil()                  
                                                        ,Nil()))                
            
                                   >(0(),y) =  [1]                              
                                            >= [1]                              
                                            =  False()                          
            
                                >(S(x),0()) =  [1]                              
                                            >= [1]                              
                                            =  True()                           
            
                               >(S(x),S(y)) =  [1]                              
                                            >= [1]                              
                                            =  >(x,y)                           
            
                         app(Cons(x,xs),ys) =  [1] xs + [1] ys + [1]            
                                            >= [1] xs + [1] ys + [1]            
                                            =  Cons(x,app(xs,ys))               
            
                              app(Nil(),ys) =  [1] ys + [0]                     
                                            >= [1] ys + [0]                     
                                            =  ys                               
            
                      part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [0]          
                                            >= [1] xs1 + [1] xs2 + [0]          
                                            =  app(xs1,xs2)                     
            
                part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            =  part[Ite](>(x',x)                
                                                        ,x'                     
                                                        ,Cons(x,xs)             
                                                        ,xs1                    
                                                        ,xs2)                   
            
                   part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [0] 
                                            =  part(x',xs,xs1,xs2)              
            
                    part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            =  part(x',xs,xs1,Cons(x,xs2))      
            
                          part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            =  part[False][Ite](<(x',x)         
                                                               ,x'              
                                                               ,Cons(x,xs)      
                                                               ,xs1             
                                                               ,xs2)            
            
                           part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                        ,x'                                     
                                ,Cons(x,xs)                                     
                                       ,xs1                                     
                                      ,xs2)                                     
                                            >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            =  part(x',xs,Cons(x,xs1),xs2)      
            
      *** 1.1.1.1.1.1.2.1.1.1.1.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x,Nil(),xs1,xs2) -> c_5()
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.2.1.1.1.1.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x,Nil(),xs1,xs2) -> c_5()
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:part#(x,Nil(),xs1,xs2) -> c_5()
                 
              
              2:W:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):6
                 -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):5
              
              3:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5():1
              
              4:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5():1
              
              5:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):4
                 -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):3
              
              6:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
                 -->_1 part#(x,Nil(),xs1,xs2) -> c_5():1
              
              7:W:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                 -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):8
              
              8:W:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                 -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):7
                 -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              7: qs#(x',Cons(x,xs)) ->                                    
                   c_7(quicksort#(xs))                                    
              8: quicksort#(Cons(x                                        
                                ,Cons(x',xs))) -> c_8(qs#(x               
                                                         ,part(x          
                                                              ,Cons(x',xs)
                                                              ,Nil()      
                                                              ,Nil()))    
                                                     ,part#(x             
                                                           ,Cons(x',xs)   
                                                           ,Nil()         
                                                           ,Nil()))       
              2: part#(x',Cons(x,xs),xs1,xs2) ->                          
                   c_6(part[Ite]#(>(x',x)                                 
                                 ,x'                                      
                                 ,Cons(x,xs)                              
                                 ,xs1                                     
                                 ,xs2))                                   
              6: part[Ite]#(True()                                        
                           ,x'                                            
                           ,Cons(x,xs)                                    
                           ,xs1                                           
                           ,xs2) -> c_20(part#(x'                         
                                              ,xs                         
                                              ,Cons(x,xs1)                
                                              ,xs2))                      
              4: part[False][Ite]#(True()                                 
                                  ,x'                                     
                                  ,Cons(x,xs)                             
                                  ,xs1                                    
                                  ,xs2) -> c_18(part#(x'                  
                                                     ,xs                  
                                                     ,xs1                 
                                                     ,Cons(x,xs2)))       
              5: part[Ite]#(False()                                       
                           ,x'                                            
                           ,Cons(x,xs)                                    
                           ,xs1                                           
                           ,xs2) ->                                       
                   c_19(part[False][Ite]#(<(x',x)                         
                                         ,x'                              
                                         ,Cons(x,xs)                      
                                         ,xs1                             
                                         ,xs2))                           
              3: part[False][Ite]#(False()                                
                                  ,x'                                     
                                  ,Cons(x,xs)                             
                                  ,xs1                                    
                                  ,xs2) -> c_17(part#(x'                  
                                                     ,xs                  
                                                     ,xs1                 
                                                     ,xs2))               
              1: part#(x,Nil(),xs1,xs2) -> c_5()                          
      *** 1.1.1.1.1.1.2.1.1.1.1.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
    *** 1.1.1.1.1.1.2.1.1.1.2 Progress [(?,O(n^2))]  ***
        Considered Problem:
          Strict DP Rules:
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Strict TRS Rules:
            
          Weak DP Rules:
            part#(x,Nil(),xs1,xs2) -> c_5()
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        Applied Processor:
          RemoveWeakSuffixes
        Proof:
          Consider the dependency graph
            1:S:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
               -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):8
               -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):7
            
            2:S:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
               -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):3
            
            3:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
               -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):2
               -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
            
            4:W:part#(x,Nil(),xs1,xs2) -> c_5()
               
            
            5:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
               -->_1 part#(x,Nil(),xs1,xs2) -> c_5():4
               -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
            
            6:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
               -->_1 part#(x,Nil(),xs1,xs2) -> c_5():4
               -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
            
            7:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
               -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):6
               -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):5
            
            8:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
               -->_1 part#(x,Nil(),xs1,xs2) -> c_5():4
               -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
            
          The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
            4: part#(x,Nil(),xs1,xs2) -> c_5()
    *** 1.1.1.1.1.1.2.1.1.1.2.1 Progress [(?,O(n^2))]  ***
        Considered Problem:
          Strict DP Rules:
            part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
          Strict TRS Rules:
            
          Weak DP Rules:
            part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
            part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
            part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
            part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
          Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
            part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
            part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          Signature:
            {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
          Obligation:
            Innermost
            basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
        Applied Processor:
          Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
        Proof:
          We analyse the complexity of following sub-problems (R) and (S).
          Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
          
          Problem (R)
            Strict DP Rules:
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            Strict TRS Rules:
              
            Weak DP Rules:
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          
          Problem (S)
            Strict DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
      *** 1.1.1.1.1.1.2.1.1.1.2.1.1 Progress [(?,O(n^2))]  ***
          Considered Problem:
            Strict DP Rules:
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            Strict TRS Rules:
              
            Weak DP Rules:
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
          Proof:
            We decompose the input problem according to the dependency graph into the upper component
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            and a lower component
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            Further, following extension rules are added to the lower component.
              qs#(x',Cons(x,xs)) -> quicksort#(xs)
              quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
              quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
        *** 1.1.1.1.1.1.2.1.1.1.2.1.1.1 Progress [(?,O(n^1))]  ***
            Considered Problem:
              Strict DP Rules:
                quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
              Strict TRS Rules:
                
              Weak DP Rules:
                qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
            Proof:
              We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
                1: quicksort#(Cons(x                                        
                                  ,Cons(x',xs))) -> c_8(qs#(x               
                                                           ,part(x          
                                                                ,Cons(x',xs)
                                                                ,Nil()      
                                                                ,Nil()))    
                                                       ,part#(x             
                                                             ,Cons(x',xs)   
                                                             ,Nil()         
                                                             ,Nil()))       
                
              Consider the set of all dependency pairs
                1: quicksort#(Cons(x                                        
                                  ,Cons(x',xs))) -> c_8(qs#(x               
                                                           ,part(x          
                                                                ,Cons(x',xs)
                                                                ,Nil()      
                                                                ,Nil()))    
                                                       ,part#(x             
                                                             ,Cons(x',xs)   
                                                             ,Nil()         
                                                             ,Nil()))       
                2: qs#(x',Cons(x,xs)) ->                                    
                     c_7(quicksort#(xs))                                    
              Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
              SPACE(?,?)on application of the dependency pairs
                {1}
              These cover all (indirect) predecessors of dependency pairs
                {1,2}
              their number of applications is equally bounded.
              The dependency pairs are shifted into the weak component.
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))]  ***
              Considered Problem:
                Strict DP Rules:
                  quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                Strict TRS Rules:
                  
                Weak DP Rules:
                  qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
              Proof:
                We apply a matrix interpretation of kind constructor based matrix interpretation:
                The following argument positions are considered usable:
                  uargs(c_7) = {1},
                  uargs(c_8) = {1}
                
                Following symbols are considered usable:
                  {>,app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
                TcT has computed the following interpretation:
                                  p(0) = [4]                                    
                                  p(<) = [0]                                    
                                  p(>) = [2]                                    
                               p(Cons) = [1] x2 + [2]                           
                              p(False) = [2]                                    
                                p(Nil) = [0]                                    
                                  p(S) = [4]                                    
                               p(True) = [2]                                    
                                p(app) = [1] x1 + [1] x2 + [0]                  
                           p(notEmpty) = [1] x1 + [0]                           
                               p(part) = [1] x2 + [1] x3 + [1] x4 + [2]         
                   p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [2]         
                          p(part[Ite]) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [0]
                                 p(qs) = [2] x1 + [0]                           
                          p(quicksort) = [4]                                    
                                 p(<#) = [4] x2 + [1]                           
                                 p(>#) = [1] x2 + [1]                           
                               p(app#) = [4] x2 + [1]                           
                          p(notEmpty#) = [0]                                    
                              p(part#) = [1] x1 + [0]                           
                  p(part[False][Ite]#) = [2] x2 + [1] x5 + [4]                  
                         p(part[Ite]#) = [1] x1 + [1] x2 + [4] x3 + [1] x5 + [1]
                                p(qs#) = [2] x2 + [0]                           
                         p(quicksort#) = [2] x1 + [2]                           
                                p(c_1) = [2] x1 + [1]                           
                                p(c_2) = [1]                                    
                                p(c_3) = [0]                                    
                                p(c_4) = [0]                                    
                                p(c_5) = [1]                                    
                                p(c_6) = [0]                                    
                                p(c_7) = [1] x1 + [2]                           
                                p(c_8) = [1] x1 + [0]                           
                                p(c_9) = [1]                                    
                               p(c_10) = [1]                                    
                               p(c_11) = [0]                                    
                               p(c_12) = [0]                                    
                               p(c_13) = [0]                                    
                               p(c_14) = [1]                                    
                               p(c_15) = [4]                                    
                               p(c_16) = [2] x1 + [1]                           
                               p(c_17) = [1]                                    
                               p(c_18) = [0]                                    
                               p(c_19) = [2] x1 + [0]                           
                               p(c_20) = [0]                                    
                
                Following rules are strictly oriented:
                quicksort#(Cons(x,Cons(x',xs))) = [2] xs + [10]           
                                                > [2] xs + [8]            
                                                = c_8(qs#(x               
                                                         ,part(x          
                                                              ,Cons(x',xs)
                                                              ,Nil()      
                                                              ,Nil()))    
                                                     ,part#(x             
                                                           ,Cons(x',xs)   
                                                           ,Nil()         
                                                           ,Nil()))       
                
                
                Following rules are (at-least) weakly oriented:
                         qs#(x',Cons(x,xs)) =  [2] xs + [4]                    
                                            >= [2] xs + [4]                    
                                            =  c_7(quicksort#(xs))             
                
                                   >(0(),y) =  [2]                             
                                            >= [2]                             
                                            =  False()                         
                
                                >(S(x),0()) =  [2]                             
                                            >= [2]                             
                                            =  True()                          
                
                               >(S(x),S(y)) =  [2]                             
                                            >= [2]                             
                                            =  >(x,y)                          
                
                         app(Cons(x,xs),ys) =  [1] xs + [1] ys + [2]           
                                            >= [1] xs + [1] ys + [2]           
                                            =  Cons(x,app(xs,ys))              
                
                              app(Nil(),ys) =  [1] ys + [0]                    
                                            >= [1] ys + [0]                    
                                            =  ys                              
                
                      part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [2]         
                                            >= [1] xs1 + [1] xs2 + [0]         
                                            =  app(xs1,xs2)                    
                
                part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [4]
                                            >= [1] xs + [1] xs1 + [1] xs2 + [4]
                                            =  part[Ite](>(x',x)               
                                                        ,x'                    
                                                        ,Cons(x,xs)            
                                                        ,xs1                   
                                                        ,xs2)                  
                
                   part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [4]
                                        ,x'                                    
                                ,Cons(x,xs)                                    
                                       ,xs1                                    
                                      ,xs2)                                    
                                            >= [1] xs + [1] xs1 + [1] xs2 + [2]
                                            =  part(x',xs,xs1,xs2)             
                
                    part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [4]
                                        ,x'                                    
                                ,Cons(x,xs)                                    
                                       ,xs1                                    
                                      ,xs2)                                    
                                            >= [1] xs + [1] xs1 + [1] xs2 + [4]
                                            =  part(x',xs,xs1,Cons(x,xs2))     
                
                          part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [4]
                                        ,x'                                    
                                ,Cons(x,xs)                                    
                                       ,xs1                                    
                                      ,xs2)                                    
                                            >= [1] xs + [1] xs1 + [1] xs2 + [4]
                                            =  part[False][Ite](<(x',x)        
                                                               ,x'             
                                                               ,Cons(x,xs)     
                                                               ,xs1            
                                                               ,xs2)           
                
                           part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [4]
                                        ,x'                                    
                                ,Cons(x,xs)                                    
                                       ,xs1                                    
                                      ,xs2)                                    
                                            >= [1] xs + [1] xs1 + [1] xs2 + [4]
                                            =  part(x',xs,Cons(x,xs1),xs2)     
                
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                  quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                Assumption
              Proof:
                ()
          
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                  quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                RemoveWeakSuffixes
              Proof:
                Consider the dependency graph
                  1:W:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                     -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):2
                  
                  2:W:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                     -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):1
                  
                The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
                  1: qs#(x',Cons(x,xs)) ->                                    
                       c_7(quicksort#(xs))                                    
                  2: quicksort#(Cons(x                                        
                                    ,Cons(x',xs))) -> c_8(qs#(x               
                                                             ,part(x          
                                                                  ,Cons(x',xs)
                                                                  ,Nil()      
                                                                  ,Nil()))    
                                                         ,part#(x             
                                                               ,Cons(x',xs)   
                                                               ,Nil()         
                                                               ,Nil()))       
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                EmptyProcessor
              Proof:
                The problem is already closed. The intended complexity is O(1).
          
        *** 1.1.1.1.1.1.2.1.1.1.2.1.1.2 Progress [(?,O(n^1))]  ***
            Considered Problem:
              Strict DP Rules:
                part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              Strict TRS Rules:
                
              Weak DP Rules:
                part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                qs#(x',Cons(x,xs)) -> quicksort#(xs)
                quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
            Proof:
              We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
                1: part#(x',Cons(x,xs),xs1,xs2) ->
                     c_6(part[Ite]#(>(x',x)       
                                   ,x'            
                                   ,Cons(x,xs)    
                                   ,xs1           
                                   ,xs2))         
                
              Consider the set of all dependency pairs
                1: part#(x',Cons(x,xs),xs1,xs2) ->                      
                     c_6(part[Ite]#(>(x',x)                             
                                   ,x'                                  
                                   ,Cons(x,xs)                          
                                   ,xs1                                 
                                   ,xs2))                               
                2: part[False][Ite]#(False()                            
                                    ,x'                                 
                                    ,Cons(x,xs)                         
                                    ,xs1                                
                                    ,xs2) -> c_17(part#(x'              
                                                       ,xs              
                                                       ,xs1             
                                                       ,xs2))           
                3: part[False][Ite]#(True()                             
                                    ,x'                                 
                                    ,Cons(x,xs)                         
                                    ,xs1                                
                                    ,xs2) -> c_18(part#(x'              
                                                       ,xs              
                                                       ,xs1             
                                                       ,Cons(x,xs2)))   
                4: part[Ite]#(False()                                   
                             ,x'                                        
                             ,Cons(x,xs)                                
                             ,xs1                                       
                             ,xs2) ->                                   
                     c_19(part[False][Ite]#(<(x',x)                     
                                           ,x'                          
                                           ,Cons(x,xs)                  
                                           ,xs1                         
                                           ,xs2))                       
                5: part[Ite]#(True()                                    
                             ,x'                                        
                             ,Cons(x,xs)                                
                             ,xs1                                       
                             ,xs2) -> c_20(part#(x'                     
                                                ,xs                     
                                                ,Cons(x,xs1)            
                                                ,xs2))                  
                6: qs#(x',Cons(x,xs)) ->                                
                     quicksort#(xs)                                     
                7: quicksort#(Cons(x                                    
                                  ,Cons(x',xs))) -> part#(x             
                                                         ,Cons(x',xs)   
                                                         ,Nil()         
                                                         ,Nil())        
                8: quicksort#(Cons(x                                    
                                  ,Cons(x',xs))) -> qs#(x               
                                                       ,part(x          
                                                            ,Cons(x',xs)
                                                            ,Nil()      
                                                            ,Nil()))    
              Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
              SPACE(?,?)on application of the dependency pairs
                {1}
              These cover all (indirect) predecessors of dependency pairs
                {1,2,3,4,5}
              their number of applications is equally bounded.
              The dependency pairs are shifted into the weak component.
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.2.1 Progress [(?,O(n^1))]  ***
              Considered Problem:
                Strict DP Rules:
                  part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                Strict TRS Rules:
                  
                Weak DP Rules:
                  part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                  part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                  part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                  part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                  qs#(x',Cons(x,xs)) -> quicksort#(xs)
                  quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                  quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
              Proof:
                We apply a matrix interpretation of kind constructor based matrix interpretation:
                The following argument positions are considered usable:
                  uargs(c_6) = {1},
                  uargs(c_17) = {1},
                  uargs(c_18) = {1},
                  uargs(c_19) = {1},
                  uargs(c_20) = {1}
                
                Following symbols are considered usable:
                  {app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
                TcT has computed the following interpretation:
                                  p(0) = [2]                           
                                  p(<) = [2] x1 + [0]                  
                                  p(>) = [0]                           
                               p(Cons) = [1] x2 + [1]                  
                              p(False) = [0]                           
                                p(Nil) = [0]                           
                                  p(S) = [0]                           
                               p(True) = [0]                           
                                p(app) = [1] x1 + [1] x2 + [0]         
                           p(notEmpty) = [1] x1 + [1]                  
                               p(part) = [1] x2 + [1] x3 + [1] x4 + [0]
                   p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                          p(part[Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]
                                 p(qs) = [0]                           
                          p(quicksort) = [4] x1 + [0]                  
                                 p(<#) = [1] x1 + [0]                  
                                 p(>#) = [1] x1 + [0]                  
                               p(app#) = [2] x2 + [2]                  
                          p(notEmpty#) = [0]                           
                              p(part#) = [1] x2 + [1]                  
                  p(part[False][Ite]#) = [1] x3 + [0]                  
                         p(part[Ite]#) = [1] x3 + [0]                  
                                p(qs#) = [4] x2 + [0]                  
                         p(quicksort#) = [4] x1 + [4]                  
                                p(c_1) = [0]                           
                                p(c_2) = [1]                           
                                p(c_3) = [2]                           
                                p(c_4) = [1]                           
                                p(c_5) = [0]                           
                                p(c_6) = [1] x1 + [0]                  
                                p(c_7) = [2] x1 + [0]                  
                                p(c_8) = [4]                           
                                p(c_9) = [0]                           
                               p(c_10) = [0]                           
                               p(c_11) = [0]                           
                               p(c_12) = [1]                           
                               p(c_13) = [0]                           
                               p(c_14) = [1]                           
                               p(c_15) = [2]                           
                               p(c_16) = [1] x1 + [0]                  
                               p(c_17) = [1] x1 + [0]                  
                               p(c_18) = [1] x1 + [0]                  
                               p(c_19) = [1] x1 + [0]                  
                               p(c_20) = [1] x1 + [0]                  
                
                Following rules are strictly oriented:
                part#(x',Cons(x,xs),xs1,xs2) = [1] xs + [2]             
                                             > [1] xs + [1]             
                                             = c_6(part[Ite]#(>(x',x)   
                                                             ,x'        
                                                             ,Cons(x,xs)
                                                             ,xs1       
                                                             ,xs2))     
                
                
                Following rules are (at-least) weakly oriented:
                      part[False][Ite]#(False() =  [1] xs + [1]                     
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1]                     
                                                =  c_17(part#(x',xs,xs1,xs2))       
                
                       part[False][Ite]#(True() =  [1] xs + [1]                     
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1]                     
                                                =  c_18(part#(x'                    
                                                             ,xs                    
                                                             ,xs1                   
                                                             ,Cons(x,xs2)))         
                
                             part[Ite]#(False() =  [1] xs + [1]                     
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1]                     
                                                =  c_19(part[False][Ite]#(<(x',x)   
                                                                         ,x'        
                                                                         ,Cons(x,xs)
                                                                         ,xs1       
                                                                         ,xs2))     
                
                              part[Ite]#(True() =  [1] xs + [1]                     
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1]                     
                                                =  c_20(part#(x'                    
                                                             ,xs                    
                                                             ,Cons(x,xs1)           
                                                             ,xs2))                 
                
                             qs#(x',Cons(x,xs)) =  [4] xs + [4]                     
                                                >= [4] xs + [4]                     
                                                =  quicksort#(xs)                   
                
                quicksort#(Cons(x,Cons(x',xs))) =  [4] xs + [12]                    
                                                >= [1] xs + [2]                     
                                                =  part#(x,Cons(x',xs),Nil(),Nil()) 
                
                quicksort#(Cons(x,Cons(x',xs))) =  [4] xs + [12]                    
                                                >= [4] xs + [4]                     
                                                =  qs#(x                            
                                                      ,part(x                       
                                                           ,Cons(x',xs)             
                                                           ,Nil()                   
                                                           ,Nil()))                 
                
                             app(Cons(x,xs),ys) =  [1] xs + [1] ys + [1]            
                                                >= [1] xs + [1] ys + [1]            
                                                =  Cons(x,app(xs,ys))               
                
                                  app(Nil(),ys) =  [1] ys + [0]                     
                                                >= [1] ys + [0]                     
                                                =  ys                               
                
                          part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [0]          
                                                >= [1] xs1 + [1] xs2 + [0]          
                                                =  app(xs1,xs2)                     
                
                    part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                                >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                                =  part[Ite](>(x',x)                
                                                            ,x'                     
                                                            ,Cons(x,xs)             
                                                            ,xs1                    
                                                            ,xs2)                   
                
                       part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1] xs1 + [1] xs2 + [0] 
                                                =  part(x',xs,xs1,xs2)              
                
                        part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                                =  part(x',xs,xs1,Cons(x,xs2))      
                
                              part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                                =  part[False][Ite](<(x',x)         
                                                                   ,x'              
                                                                   ,Cons(x,xs)      
                                                                   ,xs1             
                                                                   ,xs2)            
                
                               part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [1] 
                                            ,x'                                     
                                    ,Cons(x,xs)                                     
                                           ,xs1                                     
                                          ,xs2)                                     
                                                >= [1] xs + [1] xs1 + [1] xs2 + [1] 
                                                =  part(x',xs,Cons(x,xs1),xs2)      
                
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.2.1.1 Progress [(?,O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                  part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                  part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                  part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                  part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                  qs#(x',Cons(x,xs)) -> quicksort#(xs)
                  quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                  quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                Assumption
              Proof:
                ()
          
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.2.2 Progress [(O(1),O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                  part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                  part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                  part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                  part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                  qs#(x',Cons(x,xs)) -> quicksort#(xs)
                  quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                  quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                RemoveWeakSuffixes
              Proof:
                Consider the dependency graph
                  1:W:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                     -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):5
                     -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):4
                  
                  2:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                     -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
                  
                  3:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                     -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
                  
                  4:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                     -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):3
                     -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):2
                  
                  5:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                     -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
                  
                  6:W:qs#(x',Cons(x,xs)) -> quicksort#(xs)
                     -->_1 quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil())):8
                     -->_1 quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil()):7
                  
                  7:W:quicksort#(Cons(x,Cons(x',xs))) -> part#(x,Cons(x',xs),Nil(),Nil())
                     -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):1
                  
                  8:W:quicksort#(Cons(x,Cons(x',xs))) -> qs#(x,part(x,Cons(x',xs),Nil(),Nil()))
                     -->_1 qs#(x',Cons(x,xs)) -> quicksort#(xs):6
                  
                The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
                  6: qs#(x',Cons(x,xs)) ->                                
                       quicksort#(xs)                                     
                  8: quicksort#(Cons(x                                    
                                    ,Cons(x',xs))) -> qs#(x               
                                                         ,part(x          
                                                              ,Cons(x',xs)
                                                              ,Nil()      
                                                              ,Nil()))    
                  7: quicksort#(Cons(x                                    
                                    ,Cons(x',xs))) -> part#(x             
                                                           ,Cons(x',xs)   
                                                           ,Nil()         
                                                           ,Nil())        
                  1: part#(x',Cons(x,xs),xs1,xs2) ->                      
                       c_6(part[Ite]#(>(x',x)                             
                                     ,x'                                  
                                     ,Cons(x,xs)                          
                                     ,xs1                                 
                                     ,xs2))                               
                  5: part[Ite]#(True()                                    
                               ,x'                                        
                               ,Cons(x,xs)                                
                               ,xs1                                       
                               ,xs2) -> c_20(part#(x'                     
                                                  ,xs                     
                                                  ,Cons(x,xs1)            
                                                  ,xs2))                  
                  3: part[False][Ite]#(True()                             
                                      ,x'                                 
                                      ,Cons(x,xs)                         
                                      ,xs1                                
                                      ,xs2) -> c_18(part#(x'              
                                                         ,xs              
                                                         ,xs1             
                                                         ,Cons(x,xs2)))   
                  4: part[Ite]#(False()                                   
                               ,x'                                        
                               ,Cons(x,xs)                                
                               ,xs1                                       
                               ,xs2) ->                                   
                       c_19(part[False][Ite]#(<(x',x)                     
                                             ,x'                          
                                             ,Cons(x,xs)                  
                                             ,xs1                         
                                             ,xs2))                       
                  2: part[False][Ite]#(False()                            
                                      ,x'                                 
                                      ,Cons(x,xs)                         
                                      ,xs1                                
                                      ,xs2) -> c_17(part#(x'              
                                                         ,xs              
                                                         ,xs1             
                                                         ,xs2))           
          *** 1.1.1.1.1.1.2.1.1.1.2.1.1.2.2.1 Progress [(O(1),O(1))]  ***
              Considered Problem:
                Strict DP Rules:
                  
                Strict TRS Rules:
                  
                Weak DP Rules:
                  
                Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                  part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                  part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                  part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                  part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                  part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
                Signature:
                  {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
                Obligation:
                  Innermost
                  basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
              Applied Processor:
                EmptyProcessor
              Proof:
                The problem is already closed. The intended complexity is O(1).
          
      *** 1.1.1.1.1.1.2.1.1.1.2.1.2 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Strict TRS Rules:
              
            Weak DP Rules:
              part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
              part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
              part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:S:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                 -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):2
              
              2:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                 -->_2 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
                 -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):1
              
              3:W:part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2)):7
                 -->_1 part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2)):6
              
              4:W:part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
              
              5:W:part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2)))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
              
              6:W:part[Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_19(part[False][Ite]#(<(x',x),x',Cons(x,xs),xs1,xs2))
                 -->_1 part[False][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,xs1,Cons(x,xs2))):5
                 -->_1 part[False][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(part#(x',xs,xs1,xs2)):4
              
              7:W:part[Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_20(part#(x',xs,Cons(x,xs1),xs2))
                 -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_6(part[Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):3
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              3: part#(x',Cons(x,xs),xs1,xs2) ->                   
                   c_6(part[Ite]#(>(x',x)                          
                                 ,x'                               
                                 ,Cons(x,xs)                       
                                 ,xs1                              
                                 ,xs2))                            
              7: part[Ite]#(True()                                 
                           ,x'                                     
                           ,Cons(x,xs)                             
                           ,xs1                                    
                           ,xs2) -> c_20(part#(x'                  
                                              ,xs                  
                                              ,Cons(x,xs1)         
                                              ,xs2))               
              5: part[False][Ite]#(True()                          
                                  ,x'                              
                                  ,Cons(x,xs)                      
                                  ,xs1                             
                                  ,xs2) -> c_18(part#(x'           
                                                     ,xs           
                                                     ,xs1          
                                                     ,Cons(x,xs2)))
              6: part[Ite]#(False()                                
                           ,x'                                     
                           ,Cons(x,xs)                             
                           ,xs1                                    
                           ,xs2) ->                                
                   c_19(part[False][Ite]#(<(x',x)                  
                                         ,x'                       
                                         ,Cons(x,xs)               
                                         ,xs1                      
                                         ,xs2))                    
              4: part[False][Ite]#(False()                         
                                  ,x'                              
                                  ,Cons(x,xs)                      
                                  ,xs1                             
                                  ,xs2) -> c_17(part#(x'           
                                                     ,xs           
                                                     ,xs1          
                                                     ,xs2))        
      *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            SimplifyRHS
          Proof:
            Consider the dependency graph
              1:S:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                 -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil())):2
              
              2:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())),part#(x,Cons(x',xs),Nil(),Nil()))
                 -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):1
              
            Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
      *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
              part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
              part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            Signature:
              {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
            Obligation:
              Innermost
              basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
          Applied Processor:
            PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
          Proof:
            We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
              1: qs#(x',Cons(x,xs)) ->
                   c_7(quicksort#(xs))
              
            Consider the set of all dependency pairs
              1: qs#(x',Cons(x,xs)) ->                                    
                   c_7(quicksort#(xs))                                    
              2: quicksort#(Cons(x                                        
                                ,Cons(x',xs))) -> c_8(qs#(x               
                                                         ,part(x          
                                                              ,Cons(x',xs)
                                                              ,Nil()      
                                                              ,Nil())))   
            Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
            SPACE(?,?)on application of the dependency pairs
              {1}
            These cover all (indirect) predecessors of dependency pairs
              {1,2}
            their number of applications is equally bounded.
            The dependency pairs are shifted into the weak component.
        *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1.1.1 Progress [(?,O(n^1))]  ***
            Considered Problem:
              Strict DP Rules:
                qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
              Strict TRS Rules:
                
              Weak DP Rules:
                
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
            Proof:
              We apply a matrix interpretation of kind constructor based matrix interpretation:
              The following argument positions are considered usable:
                uargs(c_7) = {1},
                uargs(c_8) = {1}
              
              Following symbols are considered usable:
                {app,part,part[False][Ite],part[Ite],<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}
              TcT has computed the following interpretation:
                                p(0) = [4]                                    
                                p(<) = [2] x1 + [0]                           
                                p(>) = [0]                                    
                             p(Cons) = [1] x2 + [2]                           
                            p(False) = [0]                                    
                              p(Nil) = [0]                                    
                                p(S) = [1] x1 + [4]                           
                             p(True) = [0]                                    
                              p(app) = [1] x1 + [1] x2 + [0]                  
                         p(notEmpty) = [0]                                    
                             p(part) = [1] x2 + [1] x3 + [1] x4 + [0]         
                 p(part[False][Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]         
                        p(part[Ite]) = [1] x3 + [1] x4 + [1] x5 + [0]         
                               p(qs) = [1] x1 + [0]                           
                        p(quicksort) = [1]                                    
                               p(<#) = [4] x2 + [2]                           
                               p(>#) = [0]                                    
                             p(app#) = [1] x1 + [0]                           
                        p(notEmpty#) = [1]                                    
                            p(part#) = [4] x1 + [0]                           
                p(part[False][Ite]#) = [2] x1 + [1] x2 + [4] x3 + [4] x5 + [1]
                       p(part[Ite]#) = [4] x1 + [4] x5 + [0]                  
                              p(qs#) = [1] x2 + [5]                           
                       p(quicksort#) = [1] x1 + [3]                           
                              p(c_1) = [0]                                    
                              p(c_2) = [1]                                    
                              p(c_3) = [0]                                    
                              p(c_4) = [1]                                    
                              p(c_5) = [0]                                    
                              p(c_6) = [4] x1 + [2]                           
                              p(c_7) = [1] x1 + [0]                           
                              p(c_8) = [1] x1 + [0]                           
                              p(c_9) = [1]                                    
                             p(c_10) = [2]                                    
                             p(c_11) = [4]                                    
                             p(c_12) = [1]                                    
                             p(c_13) = [4]                                    
                             p(c_14) = [2]                                    
                             p(c_15) = [1]                                    
                             p(c_16) = [2] x1 + [2]                           
                             p(c_17) = [1] x1 + [0]                           
                             p(c_18) = [4]                                    
                             p(c_19) = [0]                                    
                             p(c_20) = [1] x1 + [0]                           
              
              Following rules are strictly oriented:
              qs#(x',Cons(x,xs)) = [1] xs + [7]       
                                 > [1] xs + [3]       
                                 = c_7(quicksort#(xs))
              
              
              Following rules are (at-least) weakly oriented:
              quicksort#(Cons(x,Cons(x',xs))) =  [1] xs + [7]                    
                                              >= [1] xs + [7]                    
                                              =  c_8(qs#(x                       
                                                        ,part(x                  
                                                             ,Cons(x',xs)        
                                                             ,Nil()              
                                                             ,Nil())))           
              
                           app(Cons(x,xs),ys) =  [1] xs + [1] ys + [2]           
                                              >= [1] xs + [1] ys + [2]           
                                              =  Cons(x,app(xs,ys))              
              
                                app(Nil(),ys) =  [1] ys + [0]                    
                                              >= [1] ys + [0]                    
                                              =  ys                              
              
                        part(x,Nil(),xs1,xs2) =  [1] xs1 + [1] xs2 + [0]         
                                              >= [1] xs1 + [1] xs2 + [0]         
                                              =  app(xs1,xs2)                    
              
                  part(x',Cons(x,xs),xs1,xs2) =  [1] xs + [1] xs1 + [1] xs2 + [2]
                                              >= [1] xs + [1] xs1 + [1] xs2 + [2]
                                              =  part[Ite](>(x',x)               
                                                          ,x'                    
                                                          ,Cons(x,xs)            
                                                          ,xs1                   
                                                          ,xs2)                  
              
                     part[False][Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [2]
                                          ,x'                                    
                                  ,Cons(x,xs)                                    
                                         ,xs1                                    
                                        ,xs2)                                    
                                              >= [1] xs + [1] xs1 + [1] xs2 + [0]
                                              =  part(x',xs,xs1,xs2)             
              
                      part[False][Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [2]
                                          ,x'                                    
                                  ,Cons(x,xs)                                    
                                         ,xs1                                    
                                        ,xs2)                                    
                                              >= [1] xs + [1] xs1 + [1] xs2 + [2]
                                              =  part(x',xs,xs1,Cons(x,xs2))     
              
                            part[Ite](False() =  [1] xs + [1] xs1 + [1] xs2 + [2]
                                          ,x'                                    
                                  ,Cons(x,xs)                                    
                                         ,xs1                                    
                                        ,xs2)                                    
                                              >= [1] xs + [1] xs1 + [1] xs2 + [2]
                                              =  part[False][Ite](<(x',x)        
                                                                 ,x'             
                                                                 ,Cons(x,xs)     
                                                                 ,xs1            
                                                                 ,xs2)           
              
                             part[Ite](True() =  [1] xs + [1] xs1 + [1] xs2 + [2]
                                          ,x'                                    
                                  ,Cons(x,xs)                                    
                                         ,xs1                                    
                                        ,xs2)                                    
                                              >= [1] xs + [1] xs1 + [1] xs2 + [2]
                                              =  part(x',xs,Cons(x,xs1),xs2)     
              
        *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1.1.1.1 Progress [(?,O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
              Strict TRS Rules:
                
              Weak DP Rules:
                qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              Assumption
            Proof:
              ()
        
        *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1.1.2 Progress [(O(1),O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                
              Strict TRS Rules:
                
              Weak DP Rules:
                qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              RemoveWeakSuffixes
            Proof:
              Consider the dependency graph
                1:W:qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs))
                   -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil()))):2
                
                2:W:quicksort#(Cons(x,Cons(x',xs))) -> c_8(qs#(x,part(x,Cons(x',xs),Nil(),Nil())))
                   -->_1 qs#(x',Cons(x,xs)) -> c_7(quicksort#(xs)):1
                
              The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
                1: qs#(x',Cons(x,xs)) ->                                    
                     c_7(quicksort#(xs))                                    
                2: quicksort#(Cons(x                                        
                                  ,Cons(x',xs))) -> c_8(qs#(x               
                                                           ,part(x          
                                                                ,Cons(x',xs)
                                                                ,Nil()      
                                                                ,Nil())))   
        *** 1.1.1.1.1.1.2.1.1.1.2.1.2.1.1.2.1 Progress [(O(1),O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                
              Strict TRS Rules:
                
              Weak DP Rules:
                
              Weak TRS 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,Nil(),xs1,xs2) -> app(xs1,xs2)
                part(x',Cons(x,xs),xs1,xs2) -> part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
                part[False][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,xs2)
                part[False][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,xs1,Cons(x,xs2))
                part[Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2)
                part[Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              Signature:
                {/2,app/2,notEmpty/1,part/4,part[False][Ite]/5,part[Ite]/5,qs/2,quicksort/1,<#/2,>#/2,app#/2,notEmpty#/1,part#/4,part[False][Ite]#/5,part[Ite]#/5,qs#/2,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1}
              Obligation:
                Innermost
                basic terms: {<#,>#,app#,notEmpty#,part#,part[False][Ite]#,part[Ite]#,qs#,quicksort#}/{0,Cons,False,Nil,S,True}
            Applied Processor:
              EmptyProcessor
            Proof:
              The problem is already closed. The intended complexity is O(1).