* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            even(Cons(x,Nil())) -> False()
            even(Cons(x',Cons(x,xs))) -> even(xs)
            even(Nil()) -> True()
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x,xs),Nil()) -> False()
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            even(Cons(x,Nil())) -> False()
            even(Cons(x',Cons(x,xs))) -> even(xs)
            even(Nil()) -> True()
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x,xs),Nil()) -> False()
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          even(z){z -> Cons(x,Cons(y,z))} =
            even(Cons(x,Cons(y,z))) ->^+ even(z)
              = C[even(z) = even(z){}]

** Step 1.b:1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            even(Cons(x,Nil())) -> False()
            even(Cons(x',Cons(x,xs))) -> even(xs)
            even(Nil()) -> True()
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x,xs),Nil()) -> False()
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(and) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(Cons) = [1] x2 + [0]          
               p(False) = [0]                   
                 p(Nil) = [5]                   
                p(True) = [2]                   
                 p(and) = [1] x1 + [1] x2 + [14]
                p(even) = [5] x1 + [1]          
                p(goal) = [9] x1 + [9] x2 + [2] 
                 p(lte) = [4] x1 + [2] x2 + [0] 
            p(notEmpty) = [6] x1 + [1]          
          
          Following rules are strictly oriented:
            even(Cons(x,Nil())) = [26]         
                                > [0]          
                                = False()      
          
                    even(Nil()) = [26]         
                                > [2]          
                                = True()       
          
          lte(Cons(x,xs),Nil()) = [4] xs + [10]
                                > [0]          
                                = False()      
          
                   lte(Nil(),y) = [2] y + [20] 
                                > [2]          
                                = True()       
          
                notEmpty(Nil()) = [31]         
                                > [0]          
                                = False()      
          
          
          Following rules are (at-least) weakly oriented:
                  and(False(),False()) =  [14]                  
                                       >= [0]                   
                                       =  False()               
          
                   and(False(),True()) =  [16]                  
                                       >= [0]                   
                                       =  False()               
          
                   and(True(),False()) =  [16]                  
                                       >= [0]                   
                                       =  False()               
          
                    and(True(),True()) =  [18]                  
                                       >= [2]                   
                                       =  True()                
          
             even(Cons(x',Cons(x,xs))) =  [5] xs + [1]          
                                       >= [5] xs + [1]          
                                       =  even(xs)              
          
                             goal(x,y) =  [9] x + [9] y + [2]   
                                       >= [9] x + [2] y + [15]  
                                       =  and(lte(x,y),even(x)) 
          
          lte(Cons(x',xs'),Cons(x,xs)) =  [2] xs + [4] xs' + [0]
                                       >= [2] xs + [4] xs' + [0]
                                       =  lte(xs',xs)           
          
                  notEmpty(Cons(x,xs)) =  [6] xs + [1]          
                                       >= [2]                   
                                       =  True()                
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            even(Cons(x',Cons(x,xs))) -> even(xs)
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            notEmpty(Cons(x,xs)) -> True()
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            even(Cons(x,Nil())) -> False()
            even(Nil()) -> True()
            lte(Cons(x,xs),Nil()) -> False()
            lte(Nil(),y) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(and) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(Cons) = [1] x1 + [9]         
               p(False) = [8]                  
                 p(Nil) = [12]                 
                p(True) = [7]                  
                 p(and) = [1] x1 + [1] x2 + [2]
                p(even) = [8]                  
                p(goal) = [1] x1 + [8]         
                 p(lte) = [11]                 
            p(notEmpty) = [2] x1 + [0]         
          
          Following rules are strictly oriented:
          notEmpty(Cons(x,xs)) = [2] x + [18]
                               > [7]         
                               = True()      
          
          
          Following rules are (at-least) weakly oriented:
                  and(False(),False()) =  [18]                 
                                       >= [8]                  
                                       =  False()              
          
                   and(False(),True()) =  [17]                 
                                       >= [8]                  
                                       =  False()              
          
                   and(True(),False()) =  [17]                 
                                       >= [8]                  
                                       =  False()              
          
                    and(True(),True()) =  [16]                 
                                       >= [7]                  
                                       =  True()               
          
                   even(Cons(x,Nil())) =  [8]                  
                                       >= [8]                  
                                       =  False()              
          
             even(Cons(x',Cons(x,xs))) =  [8]                  
                                       >= [8]                  
                                       =  even(xs)             
          
                           even(Nil()) =  [8]                  
                                       >= [7]                  
                                       =  True()               
          
                             goal(x,y) =  [1] x + [8]          
                                       >= [21]                 
                                       =  and(lte(x,y),even(x))
          
                 lte(Cons(x,xs),Nil()) =  [11]                 
                                       >= [8]                  
                                       =  False()              
          
          lte(Cons(x',xs'),Cons(x,xs)) =  [11]                 
                                       >= [11]                 
                                       =  lte(xs',xs)          
          
                          lte(Nil(),y) =  [11]                 
                                       >= [7]                  
                                       =  True()               
          
                       notEmpty(Nil()) =  [24]                 
                                       >= [8]                  
                                       =  False()              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            even(Cons(x',Cons(x,xs))) -> even(xs)
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            even(Cons(x,Nil())) -> False()
            even(Nil()) -> True()
            lte(Cons(x,xs),Nil()) -> False()
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(and) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(Cons) = [1] x1 + [1] x2 + [2]
               p(False) = [2]                  
                 p(Nil) = [2]                  
                p(True) = [12]                 
                 p(and) = [1] x1 + [1] x2 + [4]
                p(even) = [4] x1 + [6]         
                p(goal) = [9] x1 + [3] x2 + [1]
                 p(lte) = [5] x1 + [12]        
            p(notEmpty) = [12]                 
          
          Following rules are strictly oriented:
             even(Cons(x',Cons(x,xs))) = [4] x + [4] x' + [4] xs + [22]
                                       > [4] xs + [6]                  
                                       = even(xs)                      
          
          lte(Cons(x',xs'),Cons(x,xs)) = [5] x' + [5] xs' + [22]       
                                       > [5] xs' + [12]                
                                       = lte(xs',xs)                   
          
          
          Following rules are (at-least) weakly oriented:
           and(False(),False()) =  [8]                  
                                >= [2]                  
                                =  False()              
          
            and(False(),True()) =  [18]                 
                                >= [2]                  
                                =  False()              
          
            and(True(),False()) =  [18]                 
                                >= [2]                  
                                =  False()              
          
             and(True(),True()) =  [28]                 
                                >= [12]                 
                                =  True()               
          
            even(Cons(x,Nil())) =  [4] x + [22]         
                                >= [2]                  
                                =  False()              
          
                    even(Nil()) =  [14]                 
                                >= [12]                 
                                =  True()               
          
                      goal(x,y) =  [9] x + [3] y + [1]  
                                >= [9] x + [22]         
                                =  and(lte(x,y),even(x))
          
          lte(Cons(x,xs),Nil()) =  [5] x + [5] xs + [22]
                                >= [2]                  
                                =  False()              
          
                   lte(Nil(),y) =  [22]                 
                                >= [12]                 
                                =  True()               
          
           notEmpty(Cons(x,xs)) =  [12]                 
                                >= [12]                 
                                =  True()               
          
                notEmpty(Nil()) =  [12]                 
                                >= [2]                  
                                =  False()              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            goal(x,y) -> and(lte(x,y),even(x))
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            even(Cons(x,Nil())) -> False()
            even(Cons(x',Cons(x,xs))) -> even(xs)
            even(Nil()) -> True()
            lte(Cons(x,xs),Nil()) -> False()
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(and) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(Cons) = [1] x1 + [1] x2 + [1] 
               p(False) = [0]                   
                 p(Nil) = [3]                   
                p(True) = [8]                   
                 p(and) = [1] x1 + [1] x2 + [1] 
                p(even) = [4] x1 + [4]          
                p(goal) = [10] x1 + [8] x2 + [8]
                 p(lte) = [2] x1 + [3] x2 + [2] 
            p(notEmpty) = [8] x1 + [6]          
          
          Following rules are strictly oriented:
          goal(x,y) = [10] x + [8] y + [8] 
                    > [6] x + [3] y + [7]  
                    = and(lte(x,y),even(x))
          
          
          Following rules are (at-least) weakly oriented:
                  and(False(),False()) =  [1]                                    
                                       >= [0]                                    
                                       =  False()                                
          
                   and(False(),True()) =  [9]                                    
                                       >= [0]                                    
                                       =  False()                                
          
                   and(True(),False()) =  [9]                                    
                                       >= [0]                                    
                                       =  False()                                
          
                    and(True(),True()) =  [17]                                   
                                       >= [8]                                    
                                       =  True()                                 
          
                   even(Cons(x,Nil())) =  [4] x + [20]                           
                                       >= [0]                                    
                                       =  False()                                
          
             even(Cons(x',Cons(x,xs))) =  [4] x + [4] x' + [4] xs + [12]         
                                       >= [4] xs + [4]                           
                                       =  even(xs)                               
          
                           even(Nil()) =  [16]                                   
                                       >= [8]                                    
                                       =  True()                                 
          
                 lte(Cons(x,xs),Nil()) =  [2] x + [2] xs + [13]                  
                                       >= [0]                                    
                                       =  False()                                
          
          lte(Cons(x',xs'),Cons(x,xs)) =  [3] x + [2] x' + [3] xs + [2] xs' + [7]
                                       >= [3] xs + [2] xs' + [2]                 
                                       =  lte(xs',xs)                            
          
                          lte(Nil(),y) =  [3] y + [8]                            
                                       >= [8]                                    
                                       =  True()                                 
          
                  notEmpty(Cons(x,xs)) =  [8] x + [8] xs + [14]                  
                                       >= [8]                                    
                                       =  True()                                 
          
                       notEmpty(Nil()) =  [30]                                   
                                       >= [0]                                    
                                       =  False()                                
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            even(Cons(x,Nil())) -> False()
            even(Cons(x',Cons(x,xs))) -> even(xs)
            even(Nil()) -> True()
            goal(x,y) -> and(lte(x,y),even(x))
            lte(Cons(x,xs),Nil()) -> False()
            lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
            lte(Nil(),y) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False
            ,Nil,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))