*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        goal(xs) -> ordered(xs)
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        ordered(Cons(x,Nil())) -> True()
        ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs)))
        ordered(Nil()) -> True()
      Weak DP Rules:
        
      Weak TRS Rules:
        <(x,0()) -> False()
        <(0(),S(y)) -> True()
        <(S(x),S(y)) -> <(x,y)
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs)
      Signature:
        { [0]        
               = ordered(xs)
      
      
      Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                              
                                        >= [0]                              
                                        =  False()                          
      
                            <(0(),S(y)) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
      
                           <(S(x),S(y)) =  [0]                              
                                        >= [0]                              
                                        =  <(x,y)                           
      
                   notEmpty(Cons(x,xs)) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
      
                        notEmpty(Nil()) =  [0]                              
                                        >= [0]                              
                                        =  False()                          
      
                 ordered(Cons(x,Nil())) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
      
           ordered(Cons(x',Cons(x,xs))) =  [0]                              
                                        >= [0]                              
                                        =  ordered[Ite](<(x',x)             
                                                       ,Cons(x',Cons(x,xs)))
      
                         ordered(Nil()) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
      
               ordered[Ite](False(),xs) =  [0]                              
                                        >= [0]                              
                                        =  False()                          
      
                    ordered[Ite](True() =  [0]                              
                  ,Cons(x',Cons(x,xs)))                                     
                                        >= [0]                              
                                        =  ordered(xs)                      
      
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        ordered(Cons(x,Nil())) -> True()
        ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs)))
        ordered(Nil()) -> True()
      Weak DP Rules:
        
      Weak TRS Rules:
        <(x,0()) -> False()
        <(0(),S(y)) -> True()
        <(S(x),S(y)) -> <(x,y)
        goal(xs) -> ordered(xs)
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs)
      Signature:
        { [0]    
                               = False()
        
        ordered(Cons(x,Nil())) = [5]    
                               > [3]    
                               = True() 
        
                ordered(Nil()) = [5]    
                               > [3]    
                               = True() 
        
        
        Following rules are (at-least) weakly oriented:
                                 <(x,0()) =  [3]                              
                                          >= [0]                              
                                          =  False()                          
        
                              <(0(),S(y)) =  [3]                              
                                          >= [3]                              
                                          =  True()                           
        
                             <(S(x),S(y)) =  [3]                              
                                          >= [3]                              
                                          =  <(x,y)                           
        
                                 goal(xs) =  [9] xs + [5]                     
                                          >= [5]                              
                                          =  ordered(xs)                      
        
                     notEmpty(Cons(x,xs)) =  [2]                              
                                          >= [3]                              
                                          =  True()                           
        
             ordered(Cons(x',Cons(x,xs))) =  [5]                              
                                          >= [5]                              
                                          =  ordered[Ite](<(x',x)             
                                                         ,Cons(x',Cons(x,xs)))
        
                 ordered[Ite](False(),xs) =  [1] xs + [1]                     
                                          >= [0]                              
                                          =  False()                          
        
                      ordered[Ite](True() =  [5]                              
                    ,Cons(x',Cons(x,xs)))                                     
                                          >= [5]                              
                                          =  ordered(xs)                      
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        notEmpty(Cons(x,xs)) -> True()
        ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs)))
      Weak DP Rules:
        
      Weak TRS Rules:
        <(x,0()) -> False()
        <(0(),S(y)) -> True()
        <(S(x),S(y)) -> <(x,y)
        goal(xs) -> ordered(xs)
        notEmpty(Nil()) -> False()
        ordered(Cons(x,Nil())) -> True()
        ordered(Nil()) -> True()
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs)
      Signature:
        { [0]          
                             = True()       
        
        
        Following rules are (at-least) weakly oriented:
                                 <(x,0()) =  [15]                             
                                          >= [0]                              
                                          =  False()                          
        
                              <(0(),S(y)) =  [15]                             
                                          >= [0]                              
                                          =  True()                           
        
                             <(S(x),S(y)) =  [15]                             
                                          >= [15]                             
                                          =  <(x,y)                           
        
                                 goal(xs) =  [2] xs + [8]                     
                                          >= [2] xs + [8]                     
                                          =  ordered(xs)                      
        
                          notEmpty(Nil()) =  [10]                             
                                          >= [0]                              
                                          =  False()                          
        
                   ordered(Cons(x,Nil())) =  [16]                             
                                          >= [0]                              
                                          =  True()                           
        
             ordered(Cons(x',Cons(x,xs))) =  [2] xs + [20]                    
                                          >= [2] xs + [28]                    
                                          =  ordered[Ite](<(x',x)             
                                                         ,Cons(x',Cons(x,xs)))
        
                           ordered(Nil()) =  [10]                             
                                          >= [0]                              
                                          =  True()                           
        
                 ordered[Ite](False(),xs) =  [2] xs + [1]                     
                                          >= [0]                              
                                          =  False()                          
        
                      ordered[Ite](True() =  [2] xs + [13]                    
                    ,Cons(x',Cons(x,xs)))                                     
                                          >= [2] xs + [8]                     
                                          =  ordered(xs)                      
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs)))
      Weak DP Rules:
        
      Weak TRS Rules:
        <(x,0()) -> False()
        <(0(),S(y)) -> True()
        <(S(x),S(y)) -> <(x,y)
        goal(xs) -> ordered(xs)
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        ordered(Cons(x,Nil())) -> True()
        ordered(Nil()) -> True()
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs)
      Signature:
        { [2] x + [2] x' + [2] xs + [14]   
                                   = ordered[Ite](<(x',x)             
                                                 ,Cons(x',Cons(x,xs)))
      
      
      Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                           
                                        >= [0]                           
                                        =  False()                       
      
                            <(0(),S(y)) =  [0]                           
                                        >= [0]                           
                                        =  True()                        
      
                           <(S(x),S(y)) =  [0]                           
                                        >= [0]                           
                                        =  <(x,y)                        
      
                               goal(xs) =  [2] xs + [15]                 
                                        >= [2] xs + [13]                 
                                        =  ordered(xs)                   
      
                   notEmpty(Cons(x,xs)) =  [2] x + [2] xs + [11]         
                                        >= [0]                           
                                        =  True()                        
      
                        notEmpty(Nil()) =  [13]                          
                                        >= [0]                           
                                        =  False()                       
      
                 ordered(Cons(x,Nil())) =  [2] x + [19]                  
                                        >= [0]                           
                                        =  True()                        
      
                         ordered(Nil()) =  [17]                          
                                        >= [0]                           
                                        =  True()                        
      
               ordered[Ite](False(),xs) =  [2] xs + [10]                 
                                        >= [0]                           
                                        =  False()                       
      
                    ordered[Ite](True() =  [2] x + [2] x' + [2] xs + [14]
                  ,Cons(x',Cons(x,xs)))                                  
                                        >= [2] xs + [13]                 
                                        =  ordered(xs)                   
      
*** 1.1.1.1.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)
        goal(xs) -> ordered(xs)
        notEmpty(Cons(x,xs)) -> True()
        notEmpty(Nil()) -> False()
        ordered(Cons(x,Nil())) -> True()
        ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs)))
        ordered(Nil()) -> True()
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs)
      Signature:
        {