*** 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,xs)) -> ordered(xs)
      Signature:
        { [0]   
                               = True()
        
        
        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 + [0]                     
                                        >= [2] xs + [0]                     
                                        =  ordered(xs)                      
        
                   notEmpty(Cons(x,xs)) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
        
                        notEmpty(Nil()) =  [0]                              
                                        >= [0]                              
                                        =  False()                          
        
           ordered(Cons(x',Cons(x,xs))) =  [2] xs + [16]                    
                                        >= [2] xs + [16]                    
                                        =  ordered[Ite](<(x',x)             
                                                       ,Cons(x',Cons(x,xs)))
        
                         ordered(Nil()) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
        
               ordered[Ite](False(),xs) =  [2] xs + [0]                     
                                        >= [0]                              
                                        =  False()                          
        
        ordered[Ite](True(),Cons(x,xs)) =  [2] xs + [8]                     
                                        >= [2] xs + [0]                     
                                        =  ordered(xs)                      
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.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',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(Cons(x,Nil())) -> True()
        ordered[Ite](False(),xs) -> False()
        ordered[Ite](True(),Cons(x,xs)) -> ordered(xs)
      Signature:
        { [2] xs + [3]
                        = ordered(xs) 
        
        notEmpty(Nil()) = [28]        
                        > [0]         
                        = False()     
        
         ordered(Nil()) = [9]         
                        > [5]         
                        = True()      
        
        
        Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [11]                             
                                        >= [0]                              
                                        =  False()                          
        
                            <(0(),S(y)) =  [11]                             
                                        >= [5]                              
                                        =  True()                           
        
                           <(S(x),S(y)) =  [11]                             
                                        >= [11]                             
                                        =  <(x,y)                           
        
                   notEmpty(Cons(x,xs)) =  [8] x + [8] xs + [4]             
                                        >= [5]                              
                                        =  True()                           
        
                 ordered(Cons(x,Nil())) =  [2] x + [9]                      
                                        >= [5]                              
                                        =  True()                           
        
           ordered(Cons(x',Cons(x,xs))) =  [2] x + [2] x' + [2] xs + [3]    
                                        >= [2] x + [2] x' + [2] xs + [12]   
                                        =  ordered[Ite](<(x',x)             
                                                       ,Cons(x',Cons(x,xs)))
        
               ordered[Ite](False(),xs) =  [2] xs + [1]                     
                                        >= [0]                              
                                        =  False()                          
        
        ordered[Ite](True(),Cons(x,xs)) =  [2] x + [2] xs + [6]             
                                        >= [2] xs + [3]                     
                                        =  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,xs)) -> ordered(xs)
      Signature:
        { [0]   
                             = True()
        
        
        Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [3]                              
                                        >= [0]                              
                                        =  False()                          
        
                            <(0(),S(y)) =  [3]                              
                                        >= [0]                              
                                        =  True()                           
        
                           <(S(x),S(y)) =  [3]                              
                                        >= [3]                              
                                        =  <(x,y)                           
        
                               goal(xs) =  [9]                              
                                        >= [0]                              
                                        =  ordered(xs)                      
        
                        notEmpty(Nil()) =  [2]                              
                                        >= [0]                              
                                        =  False()                          
        
                 ordered(Cons(x,Nil())) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
        
           ordered(Cons(x',Cons(x,xs))) =  [0]                              
                                        >= [3]                              
                                        =  ordered[Ite](<(x',x)             
                                                       ,Cons(x',Cons(x,xs)))
        
                         ordered(Nil()) =  [0]                              
                                        >= [0]                              
                                        =  True()                           
        
               ordered[Ite](False(),xs) =  [0]                              
                                        >= [0]                              
                                        =  False()                          
        
        ordered[Ite](True(),Cons(x,xs)) =  [0]                              
                                        >= [0]                              
                                        =  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,xs)) -> ordered(xs)
      Signature:
        { [1] xs + [16]                    
                                   = 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) =  [8] xs + [9] 
                                      >= [1] xs + [8] 
                                      =  ordered(xs)  
      
                 notEmpty(Cons(x,xs)) =  [2] xs + [20]
                                      >= [0]          
                                      =  True()       
      
                      notEmpty(Nil()) =  [12]         
                                      >= [0]          
                                      =  False()      
      
               ordered(Cons(x,Nil())) =  [20]         
                                      >= [0]          
                                      =  True()       
      
                       ordered(Nil()) =  [12]         
                                      >= [0]          
                                      =  True()       
      
             ordered[Ite](False(),xs) =  [1] xs + [0] 
                                      >= [0]          
                                      =  False()      
      
      ordered[Ite](True(),Cons(x,xs)) =  [1] xs + [8] 
                                      >= [1] xs + [8] 
                                      =  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,xs)) -> ordered(xs)
      Signature:
        {