WORST_CASE(?,O(n^1))
* Step 1: DependencyPairs 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:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          even#(Cons(x,Nil())) -> c_1()
          even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
          even#(Nil()) -> c_3()
          goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
          lte#(Cons(x,xs),Nil()) -> c_5()
          lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
          lte#(Nil(),y) -> c_7()
          notEmpty#(Cons(x,xs)) -> c_8()
          notEmpty#(Nil()) -> c_9()
        Weak DPs
          and#(False(),False()) -> c_10()
          and#(False(),True()) -> c_11()
          and#(True(),False()) -> c_12()
          and#(True(),True()) -> c_13()
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x,Nil())) -> c_1()
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            even#(Nil()) -> c_3()
            goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
            lte#(Cons(x,xs),Nil()) -> c_5()
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
            lte#(Nil(),y) -> c_7()
            notEmpty#(Cons(x,xs)) -> c_8()
            notEmpty#(Nil()) -> c_9()
        - Weak DPs:
            and#(False(),False()) -> c_10()
            and#(False(),True()) -> c_11()
            and#(True(),False()) -> c_12()
            and#(True(),True()) -> c_13()
        - 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,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons
            ,False,Nil,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,5,7,8,9}
        by application of
          Pre({1,3,5,7,8,9}) = {2,4,6}.
        Here rules are labelled as follows:
          1: even#(Cons(x,Nil())) -> c_1()
          2: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
          3: even#(Nil()) -> c_3()
          4: goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
          5: lte#(Cons(x,xs),Nil()) -> c_5()
          6: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
          7: lte#(Nil(),y) -> c_7()
          8: notEmpty#(Cons(x,xs)) -> c_8()
          9: notEmpty#(Nil()) -> c_9()
          10: and#(False(),False()) -> c_10()
          11: and#(False(),True()) -> c_11()
          12: and#(True(),False()) -> c_12()
          13: and#(True(),True()) -> c_13()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
        - Weak DPs:
            and#(False(),False()) -> c_10()
            and#(False(),True()) -> c_11()
            and#(True(),False()) -> c_12()
            and#(True(),True()) -> c_13()
            even#(Cons(x,Nil())) -> c_1()
            even#(Nil()) -> c_3()
            lte#(Cons(x,xs),Nil()) -> c_5()
            lte#(Nil(),y) -> c_7()
            notEmpty#(Cons(x,xs)) -> c_8()
            notEmpty#(Nil()) -> c_9()
        - 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,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons
            ,False,Nil,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
             -->_1 even#(Nil()) -> c_3():9
             -->_1 even#(Cons(x,Nil())) -> c_1():8
             -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
          
          2:S:goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
             -->_2 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
             -->_2 lte#(Nil(),y) -> c_7():11
             -->_2 lte#(Cons(x,xs),Nil()) -> c_5():10
             -->_3 even#(Nil()) -> c_3():9
             -->_3 even#(Cons(x,Nil())) -> c_1():8
             -->_1 and#(True(),True()) -> c_13():7
             -->_1 and#(True(),False()) -> c_12():6
             -->_1 and#(False(),True()) -> c_11():5
             -->_1 and#(False(),False()) -> c_10():4
             -->_3 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
          
          3:S:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
             -->_1 lte#(Nil(),y) -> c_7():11
             -->_1 lte#(Cons(x,xs),Nil()) -> c_5():10
             -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
          
          4:W:and#(False(),False()) -> c_10()
             
          
          5:W:and#(False(),True()) -> c_11()
             
          
          6:W:and#(True(),False()) -> c_12()
             
          
          7:W:and#(True(),True()) -> c_13()
             
          
          8:W:even#(Cons(x,Nil())) -> c_1()
             
          
          9:W:even#(Nil()) -> c_3()
             
          
          10:W:lte#(Cons(x,xs),Nil()) -> c_5()
             
          
          11:W:lte#(Nil(),y) -> c_7()
             
          
          12:W:notEmpty#(Cons(x,xs)) -> c_8()
             
          
          13:W:notEmpty#(Nil()) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          13: notEmpty#(Nil()) -> c_9()
          12: notEmpty#(Cons(x,xs)) -> c_8()
          4: and#(False(),False()) -> c_10()
          5: and#(False(),True()) -> c_11()
          6: and#(True(),False()) -> c_12()
          7: and#(True(),True()) -> c_13()
          10: lte#(Cons(x,xs),Nil()) -> c_5()
          11: lte#(Nil(),y) -> c_7()
          8: even#(Cons(x,Nil())) -> c_1()
          9: even#(Nil()) -> c_3()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(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(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,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons
            ,False,Nil,True}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
             -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
          
          2:S:goal#(x,y) -> c_4(and#(lte(x,y),even(x)),lte#(x,y),even#(x))
             -->_2 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
             -->_3 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
          
          3:S:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
             -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          goal#(x,y) -> c_4(lte#(x,y),even#(x))
* Step 5: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            goal#(x,y) -> c_4(lte#(x,y),even#(x))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(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(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,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons
            ,False,Nil,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
          goal#(x,y) -> c_4(lte#(x,y),even#(x))
          lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
* Step 6: RemoveHeads WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            goal#(x,y) -> c_4(lte#(x,y),even#(x))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons
            ,False,Nil,True}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
           -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
        
        2:S:goal#(x,y) -> c_4(lte#(x,y),even#(x))
           -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
           -->_2 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1
        
        3:S:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
           -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):3
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(2,goal#(x,y) -> c_4(lte#(x,y),even#(x)))]
* Step 7: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/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 constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1},
            uargs(c_6) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(Cons) = [1] x1 + [1] x2 + [3]
                p(False) = [0]                  
                  p(Nil) = [0]                  
                 p(True) = [0]                  
                  p(and) = [0]                  
                 p(even) = [0]                  
                 p(goal) = [0]                  
                  p(lte) = [0]                  
             p(notEmpty) = [0]                  
                 p(and#) = [0]                  
                p(even#) = [13]                 
                p(goal#) = [0]                  
                 p(lte#) = [5] x1 + [0]         
            p(notEmpty#) = [0]                  
                  p(c_1) = [0]                  
                  p(c_2) = [1] x1 + [0]         
                  p(c_3) = [0]                  
                  p(c_4) = [0]                  
                  p(c_5) = [0]                  
                  p(c_6) = [1] x1 + [0]         
                  p(c_7) = [0]                  
                  p(c_8) = [0]                  
                  p(c_9) = [0]                  
                 p(c_10) = [0]                  
                 p(c_11) = [0]                  
                 p(c_12) = [0]                  
                 p(c_13) = [0]                  
          
          Following rules are strictly oriented:
          lte#(Cons(x',xs'),Cons(x,xs)) = [5] x' + [5] xs' + [15]
                                        > [5] xs' + [0]          
                                        = c_6(lte#(xs',xs))      
          
          
          Following rules are (at-least) weakly oriented:
          even#(Cons(x',Cons(x,xs))) =  [13]          
                                     >= [13]          
                                     =  c_2(even#(xs))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
        - Weak DPs:
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/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 constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1},
            uargs(c_6) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(Cons) = [1] x1 + [1] x2 + [4]
                p(False) = [0]                  
                  p(Nil) = [0]                  
                 p(True) = [0]                  
                  p(and) = [0]                  
                 p(even) = [0]                  
                 p(goal) = [2] x1 + [0]         
                  p(lte) = [1] x2 + [1]         
             p(notEmpty) = [1] x1 + [1]         
                 p(and#) = [1] x1 + [0]         
                p(even#) = [2] x1 + [9]         
                p(goal#) = [1] x2 + [1]         
                 p(lte#) = [0]                  
            p(notEmpty#) = [2] x1 + [1]         
                  p(c_1) = [1]                  
                  p(c_2) = [1] x1 + [7]         
                  p(c_3) = [0]                  
                  p(c_4) = [1] x1 + [0]         
                  p(c_5) = [1]                  
                  p(c_6) = [1] x1 + [0]         
                  p(c_7) = [0]                  
                  p(c_8) = [1]                  
                  p(c_9) = [8]                  
                 p(c_10) = [8]                  
                 p(c_11) = [1]                  
                 p(c_12) = [2]                  
                 p(c_13) = [0]                  
          
          Following rules are strictly oriented:
          even#(Cons(x',Cons(x,xs))) = [2] x + [2] x' + [2] xs + [25]
                                     > [2] xs + [16]                 
                                     = c_2(even#(xs))                
          
          
          Following rules are (at-least) weakly oriented:
          lte#(Cons(x',xs'),Cons(x,xs)) =  [0]              
                                        >= [0]              
                                        =  c_6(lte#(xs',xs))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs))
            lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs))
        - Signature:
            {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0
            ,True/0,c_1/0,c_2/1,c_3/0,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/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(?,O(n^1))