* Step 1: Sum 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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: MI 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:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        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) = [4]          
                          p(member) = [0]          
          p(member[Ite][True][Ite]) = [1] x_1 + [0]
                        p(notEmpty) = [0]          
        
        Following rules are strictly oriented:
        goal(x,xs) = [4]         
                   > [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 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))
            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) = [0]         
                                 p(0) = [0]         
                              p(Cons) = [1] x1 + [0]
                             p(False) = [0]         
                               p(Nil) = [0]         
                                 p(S) = [1] x1 + [0]
                              p(True) = [0]         
                              p(goal) = [0]         
                            p(member) = [0]         
            p(member[Ite][True][Ite]) = [1] x1 + [0]
                          p(notEmpty) = [1]         
          
          Following rules are strictly oriented:
          notEmpty(Cons(x,xs)) = [1]    
                               > [0]    
                               = True() 
          
               notEmpty(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) =  [0]                                            
                                                        >= [0]                                            
                                                        =  member(x,xs)                                   
          
                                        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()                                         
          
        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,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) = [9]                  
                                 p(0) = [0]                  
                              p(Cons) = [1] x1 + [1] x2 + [0]
                             p(False) = [5]                  
                               p(Nil) = [0]                  
                                 p(S) = [1] x1 + [0]         
                              p(True) = [8]                  
                              p(goal) = [9] x2 + [6]         
                            p(member) = [6]                  
            p(member[Ite][True][Ite]) = [1] x1 + [3]         
                          p(notEmpty) = [4] x1 + [10]        
          
          Following rules are strictly oriented:
          member(x,Nil()) = [6]    
                          > [5]    
                          = False()
          
          
          Following rules are (at-least) weakly oriented:
                                           !EQ(0(),0()) =  [9]                                            
                                                        >= [8]                                            
                                                        =  True()                                         
          
                                          !EQ(0(),S(y)) =  [9]                                            
                                                        >= [5]                                            
                                                        =  False()                                        
          
                                          !EQ(S(x),0()) =  [9]                                            
                                                        >= [5]                                            
                                                        =  False()                                        
          
                                         !EQ(S(x),S(y)) =  [9]                                            
                                                        >= [9]                                            
                                                        =  !EQ(x,y)                                       
          
                                             goal(x,xs) =  [9] xs + [6]                                   
                                                        >= [6]                                            
                                                        =  member(x,xs)                                   
          
                                  member(x',Cons(x,xs)) =  [6]                                            
                                                        >= [12]                                           
                                                        =  member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          
          member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [8]                                            
                                                        >= [6]                                            
                                                        =  member(x',xs)                                  
          
                    member[Ite][True][Ite](True(),x,xs) =  [11]                                           
                                                        >= [8]                                            
                                                        =  True()                                         
          
                                   notEmpty(Cons(x,xs)) =  [4] x + [4] xs + [10]                          
                                                        >= [8]                                            
                                                        =  True()                                         
          
                                        notEmpty(Nil()) =  [10]                                           
                                                        >= [5]                                            
                                                        =  False()                                        
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: 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) = [0]                  
                                 p(0) = [0]                  
                              p(Cons) = [1] x1 + [1] x2 + [1]
                             p(False) = [0]                  
                               p(Nil) = [1]                  
                                 p(S) = [1] x1 + [0]         
                              p(True) = [0]                  
                              p(goal) = [1] x2 + [10]        
                            p(member) = [1] x2 + [10]        
            p(member[Ite][True][Ite]) = [1] x1 + [1] x3 + [9]
                          p(notEmpty) = [12] x1 + [0]        
          
          Following rules are strictly oriented:
          member(x',Cons(x,xs)) = [1] x + [1] xs + [11]                          
                                > [1] x + [1] xs + [10]                          
                                = member[Ite][True][Ite](!EQ(x',x),x',Cons(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)               
          
                                             goal(x,xs) =  [1] xs + [10]          
                                                        >= [1] xs + [10]          
                                                        =  member(x,xs)           
          
                                        member(x,Nil()) =  [11]                   
                                                        >= [0]                    
                                                        =  False()                
          
          member[Ite][True][Ite](False(),x',Cons(x,xs)) =  [1] x + [1] xs + [10]  
                                                        >= [1] xs + [10]          
                                                        =  member(x',xs)          
          
                    member[Ite][True][Ite](True(),x,xs) =  [1] xs + [9]           
                                                        >= [0]                    
                                                        =  True()                 
          
                                   notEmpty(Cons(x,xs)) =  [12] x + [12] xs + [12]
                                                        >= [0]                    
                                                        =  True()                 
          
                                        notEmpty(Nil()) =  [12]                   
                                                        >= [0]                    
                                                        =  False()                
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: 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))