WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            a(C(x1,x2),y) -> C(a(x1,y),a(x2,C(x1,x2)))
            a(Z(),y) -> Z()
            eqZList(C(x1,x2),C(y1,y2)) -> and(eqZList(x1,y1),eqZList(x2,y2))
            eqZList(C(x1,x2),Z()) -> False()
            eqZList(Z(),C(y1,y2)) -> False()
            eqZList(Z(),Z()) -> True()
            first(C(x1,x2)) -> x1
            second(C(x1,x2)) -> x2
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
        - Signature:
            {a/2,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,and,eqZList,first,second} and constructors {C,False
            ,True,Z}
    + 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(C) = {1,2},
          uargs(and) = {1,2}
        
        Following symbols are considered usable:
          {a,and,eqZList,first,second}
        TcT has computed the following interpretation:
                p(C) = [1] x1 + [1] x2 + [4] 
            p(False) = [8]                   
             p(True) = [5]                   
                p(Z) = [4]                   
                p(a) = [4] x1 + [6]          
              p(and) = [1] x1 + [1] x2 + [14]
          p(eqZList) = [4] x2 + [0]          
            p(first) = [4] x1 + [1]          
           p(second) = [4] x1 + [8]          
        
        Following rules are strictly oriented:
                     a(C(x1,x2),y) = [4] x1 + [4] x2 + [22]            
                                   > [4] x1 + [4] x2 + [16]            
                                   = C(a(x1,y),a(x2,C(x1,x2)))         
        
                          a(Z(),y) = [22]                              
                                   > [4]                               
                                   = Z()                               
        
        eqZList(C(x1,x2),C(y1,y2)) = [4] y1 + [4] y2 + [16]            
                                   > [4] y1 + [4] y2 + [14]            
                                   = and(eqZList(x1,y1),eqZList(x2,y2))
        
             eqZList(C(x1,x2),Z()) = [16]                              
                                   > [8]                               
                                   = False()                           
        
             eqZList(Z(),C(y1,y2)) = [4] y1 + [4] y2 + [16]            
                                   > [8]                               
                                   = False()                           
        
                  eqZList(Z(),Z()) = [16]                              
                                   > [5]                               
                                   = True()                            
        
                   first(C(x1,x2)) = [4] x1 + [4] x2 + [17]            
                                   > [1] x1 + [0]                      
                                   = x1                                
        
                  second(C(x1,x2)) = [4] x1 + [4] x2 + [24]            
                                   > [1] x2 + [0]                      
                                   = x2                                
        
        
        Following rules are (at-least) weakly oriented:
        and(False(),False()) =  [30]   
                             >= [8]    
                             =  False()
        
         and(False(),True()) =  [27]   
                             >= [8]    
                             =  False()
        
         and(True(),False()) =  [27]   
                             >= [8]    
                             =  False()
        
          and(True(),True()) =  [24]   
                             >= [5]    
                             =  True() 
        
* Step 2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            a(C(x1,x2),y) -> C(a(x1,y),a(x2,C(x1,x2)))
            a(Z(),y) -> Z()
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqZList(C(x1,x2),C(y1,y2)) -> and(eqZList(x1,y1),eqZList(x2,y2))
            eqZList(C(x1,x2),Z()) -> False()
            eqZList(Z(),C(y1,y2)) -> False()
            eqZList(Z(),Z()) -> True()
            first(C(x1,x2)) -> x1
            second(C(x1,x2)) -> x2
        - Signature:
            {a/2,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,and,eqZList,first,second} and constructors {C,False
            ,True,Z}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))