WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum.  WORST_CASE(Omega(n^1),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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: Sum.  WORST_CASE(Omega(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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:2: DecreasingLoops.  WORST_CASE(Omega(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:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          a(x,z){x -> C(x,y)} =
            a(C(x,y),z) ->^+ C(a(x,z),a(y,C(x,y)))
              = C[a(x,z) = a(x,z){}]

** Step 1.b:1: NaturalPI.  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:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        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) = 2 + x1 + x2
            p(False) = 0          
             p(True) = 0          
                p(Z) = 3          
                p(a) = 6*x1       
              p(and) = 1 + x1 + x2
          p(eqZList) = x1         
            p(first) = 12 + 2*x1  
           p(second) = 2 + 13*x1  
        
        Following rules are strictly oriented:
                     a(C(x1,x2),y) = 12 + 6*x1 + 6*x2                  
                                   > 2 + 6*x1 + 6*x2                   
                                   = C(a(x1,y),a(x2,C(x1,x2)))         
        
                          a(Z(),y) = 18                                
                                   > 3                                 
                                   = Z()                               
        
        eqZList(C(x1,x2),C(y1,y2)) = 2 + x1 + x2                       
                                   > 1 + x1 + x2                       
                                   = and(eqZList(x1,y1),eqZList(x2,y2))
        
             eqZList(C(x1,x2),Z()) = 2 + x1 + x2                       
                                   > 0                                 
                                   = False()                           
        
             eqZList(Z(),C(y1,y2)) = 3                                 
                                   > 0                                 
                                   = False()                           
        
                  eqZList(Z(),Z()) = 3                                 
                                   > 0                                 
                                   = True()                            
        
                   first(C(x1,x2)) = 16 + 2*x1 + 2*x2                  
                                   > x1                                
                                   = x1                                
        
                  second(C(x1,x2)) = 28 + 13*x1 + 13*x2                
                                   > x2                                
                                   = x2                                
        
        
        Following rules are (at-least) weakly oriented:
        and(False(),False()) =  1      
                             >= 0      
                             =  False()
        
         and(False(),True()) =  1      
                             >= 0      
                             =  False()
        
         and(True(),False()) =  1      
                             >= 0      
                             =  False()
        
          and(True(),True()) =  1      
                             >= 0      
                             =  True() 
        
** Step 1.b: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(Omega(n^1),O(n^1))