WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            goal(x,xs) -> member(x,xs)
            member(x,Nil()) -> False()
            member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
            member[Ite][True][Ite](True(),x,xs) -> True()
        - Signature:
            {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
            ,notEmpty} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(member[Ite][True][Ite]) = {1}
        
        Following symbols are considered usable:
          {!EQ,goal,member,member[Ite][True][Ite],notEmpty}
        TcT has computed the following interpretation:
                             p(!EQ) = [0]         
                               p(0) = [0]         
                            p(Cons) = [0]         
                           p(False) = [0]         
                             p(Nil) = [0]         
                               p(S) = [0]         
                            p(True) = [0]         
                            p(goal) = [8]         
                          p(member) = [0]         
          p(member[Ite][True][Ite]) = [8] x1 + [0]
                        p(notEmpty) = [0]         
        
        Following rules are strictly oriented:
        goal(x,xs) = [8]         
                   > [0]         
                   = member(x,xs)
        
        
        Following rules are (at-least) weakly oriented:
                                         !EQ(0(),0()) =  [0]                                            
                                                      >= [0]                                            
                                                      =  True()                                         
        
                                        !EQ(0(),S(y)) =  [0]                                            
                                                      >= [0]                                            
                                                      =  False()                                        
        
                                        !EQ(S(x),0()) =  [0]                                            
                                                      >= [0]                                            
                                                      =  False()                                        
        
                                       !EQ(S(x),S(y)) =  [0]                                            
                                                      >= [0]                                            
                                                      =  !EQ(x,y)                                       
        
                                      member(x,Nil()) =  [0]                                            
                                                      >= [0]                                            
                                                      =  False()                                        
        
                                member(x',Cons(x,xs)) =  [0]                                            
                                                      >= [0]                                            
                                                      =  member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
        
        member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [0]                                            
                                                      >= [0]                                            
                                                      =  member(x',xs)                                  
        
                  member[Ite][True][Ite](True(),x,xs) =  [0]                                            
                                                      >= [0]                                            
                                                      =  True()                                         
        
                                 notEmpty(Cons(x,xs)) =  [0]                                            
                                                      >= [0]                                            
                                                      =  True()                                         
        
                                      notEmpty(Nil()) =  [0]                                            
                                                      >= [0]                                            
                                                      =  False()                                        
        
* Step 2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            member(x,Nil()) -> False()
            member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            goal(x,xs) -> member(x,xs)
            member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
            member[Ite][True][Ite](True(),x,xs) -> True()
        - Signature:
            {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
            ,notEmpty} and constructors {0,Cons,False,Nil,S,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(member[Ite][True][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                               p(!EQ) = [1]                  
                                 p(0) = [1]                  
                              p(Cons) = [1] x1 + [1] x2 + [0]
                             p(False) = [0]                  
                               p(Nil) = [0]                  
                                 p(S) = [1]                  
                              p(True) = [1]                  
                              p(goal) = [2] x1 + [3] x2 + [1]
                            p(member) = [2] x2 + [0]         
            p(member[Ite][True][Ite]) = [1] x1 + [2] x3 + [0]
                          p(notEmpty) = [2] x1 + [6]         
          
          Following rules are strictly oriented:
          notEmpty(Cons(x,xs)) = [2] x + [2] xs + [6]
                               > [1]                 
                               = True()              
          
               notEmpty(Nil()) = [6]                 
                               > [0]                 
                               = False()             
          
          
          Following rules are (at-least) weakly oriented:
                                           !EQ(0(),0()) =  [1]                                            
                                                        >= [1]                                            
                                                        =  True()                                         
          
                                          !EQ(0(),S(y)) =  [1]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
                                          !EQ(S(x),0()) =  [1]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
                                         !EQ(S(x),S(y)) =  [1]                                            
                                                        >= [1]                                            
                                                        =  !EQ(x,y)                                       
          
                                             goal(x,xs) =  [2] x + [3] xs + [1]                           
                                                        >= [2] xs + [0]                                   
                                                        =  member(x,xs)                                   
          
                                        member(x,Nil()) =  [0]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
                                  member(x',Cons(x,xs)) =  [2] x + [2] xs + [0]                           
                                                        >= [2] x + [2] xs + [1]                           
                                                        =  member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          
          member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [2] x + [2] xs + [0]                           
                                                        >= [2] xs + [0]                                   
                                                        =  member(x',xs)                                  
          
                    member[Ite][True][Ite](True(),x,xs) =  [2] xs + [1]                                   
                                                        >= [1]                                            
                                                        =  True()                                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            member(x,Nil()) -> False()
            member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            goal(x,xs) -> member(x,xs)
            member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
            member[Ite][True][Ite](True(),x,xs) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
            ,notEmpty} and constructors {0,Cons,False,Nil,S,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(member[Ite][True][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                               p(!EQ) = [0]                   
                                 p(0) = [0]                   
                              p(Cons) = [4]                   
                             p(False) = [0]                   
                               p(Nil) = [0]                   
                                 p(S) = [0]                   
                              p(True) = [0]                   
                              p(goal) = [5] x1 + [9]          
                            p(member) = [1]                   
            p(member[Ite][True][Ite]) = [1] x1 + [2] x3 + [13]
                          p(notEmpty) = [4] x1 + [0]          
          
          Following rules are strictly oriented:
          member(x,Nil()) = [1]    
                          > [0]    
                          = False()
          
          
          Following rules are (at-least) weakly oriented:
                                           !EQ(0(),0()) =  [0]                                            
                                                        >= [0]                                            
                                                        =  True()                                         
          
                                          !EQ(0(),S(y)) =  [0]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
                                          !EQ(S(x),0()) =  [0]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
                                         !EQ(S(x),S(y)) =  [0]                                            
                                                        >= [0]                                            
                                                        =  !EQ(x,y)                                       
          
                                             goal(x,xs) =  [5] x + [9]                                    
                                                        >= [1]                                            
                                                        =  member(x,xs)                                   
          
                                  member(x',Cons(x,xs)) =  [1]                                            
                                                        >= [21]                                           
                                                        =  member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          
          member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [21]                                           
                                                        >= [1]                                            
                                                        =  member(x',xs)                                  
          
                    member[Ite][True][Ite](True(),x,xs) =  [2] xs + [13]                                  
                                                        >= [0]                                            
                                                        =  True()                                         
          
                                   notEmpty(Cons(x,xs)) =  [16]                                           
                                                        >= [0]                                            
                                                        =  True()                                         
          
                                        notEmpty(Nil()) =  [0]                                            
                                                        >= [0]                                            
                                                        =  False()                                        
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            goal(x,xs) -> member(x,xs)
            member(x,Nil()) -> False()
            member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
            member[Ite][True][Ite](True(),x,xs) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
            ,notEmpty} and constructors {0,Cons,False,Nil,S,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(member[Ite][True][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                               p(!EQ) = [7]                           
                                 p(0) = [8]                           
                              p(Cons) = [1] x2 + [8]                  
                             p(False) = [0]                           
                               p(Nil) = [0]                           
                                 p(S) = [1] x1 + [1]                  
                              p(True) = [0]                           
                              p(goal) = [10] x1 + [9] x2 + [13]       
                            p(member) = [6] x1 + [1] x2 + [13]        
            p(member[Ite][True][Ite]) = [1] x1 + [6] x2 + [1] x3 + [5]
                          p(notEmpty) = [2] x1 + [4]                  
          
          Following rules are strictly oriented:
          member(x',Cons(x,xs)) = [6] x' + [1] xs + [21]                         
                                > [6] x' + [1] xs + [20]                         
                                = member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          
          
          Following rules are (at-least) weakly oriented:
                                           !EQ(0(),0()) =  [7]                   
                                                        >= [0]                   
                                                        =  True()                
          
                                          !EQ(0(),S(y)) =  [7]                   
                                                        >= [0]                   
                                                        =  False()               
          
                                          !EQ(S(x),0()) =  [7]                   
                                                        >= [0]                   
                                                        =  False()               
          
                                         !EQ(S(x),S(y)) =  [7]                   
                                                        >= [7]                   
                                                        =  !EQ(x,y)              
          
                                             goal(x,xs) =  [10] x + [9] xs + [13]
                                                        >= [6] x + [1] xs + [13] 
                                                        =  member(x,xs)          
          
                                        member(x,Nil()) =  [6] x + [13]          
                                                        >= [0]                   
                                                        =  False()               
          
          member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [6] x' + [1] xs + [13]
                                                        >= [6] x' + [1] xs + [13]
                                                        =  member(x',xs)         
          
                    member[Ite][True][Ite](True(),x,xs) =  [6] x + [1] xs + [5]  
                                                        >= [0]                   
                                                        =  True()                
          
                                   notEmpty(Cons(x,xs)) =  [2] xs + [20]         
                                                        >= [0]                   
                                                        =  True()                
          
                                        notEmpty(Nil()) =  [4]                   
                                                        >= [0]                   
                                                        =  False()               
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            goal(x,xs) -> member(x,xs)
            member(x,Nil()) -> False()
            member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
            member[Ite][True][Ite](True(),x,xs) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
            ,notEmpty} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))