WORST_CASE(?,O(n^3))
* Step 1: MI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__adx(X) -> adx(X)
            a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
            a__hd(X) -> hd(X)
            a__hd(cons(X,Y)) -> mark(X)
            a__incr(X) -> incr(X)
            a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
            a__nats() -> a__adx(a__zeros())
            a__nats() -> nats()
            a__tl(X) -> tl(X)
            a__tl(cons(X,Y)) -> mark(Y)
            a__zeros() -> cons(0(),zeros())
            a__zeros() -> zeros()
            mark(0()) -> 0()
            mark(adx(X)) -> a__adx(mark(X))
            mark(cons(X1,X2)) -> cons(X1,X2)
            mark(hd(X)) -> a__hd(mark(X))
            mark(incr(X)) -> a__incr(mark(X))
            mark(nats()) -> a__nats()
            mark(s(X)) -> s(X)
            mark(tl(X)) -> a__tl(mark(X))
            mark(zeros()) -> a__zeros()
        - Signature:
            {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1
            ,tl/1,zeros/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros
            ,mark} and constructors {0,adx,cons,hd,incr,nats,s,tl,zeros}
    + Applied Processor:
        MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
    + Details:
        We apply a matrix interpretation of kind Automaton Nothing:
        
        
        Following symbols are considered usable:
          all
        TcT has computed the following interpretation:
                 p(0) = [0]                            
                        [0]                            
                        [0]                            
            p(a__adx) = [1 2 0]       [1]              
                        [0 1 2] x_1 + [0]              
                        [0 0 1]       [1]              
             p(a__hd) = [1 1 0]       [4]              
                        [0 1 3] x_1 + [1]              
                        [0 0 1]       [2]              
           p(a__incr) = [1 0 0]       [2]              
                        [0 1 0] x_1 + [1]              
                        [0 0 1]       [0]              
           p(a__nats) = [7]                            
                        [6]                            
                        [3]                            
             p(a__tl) = [1 3 0]       [4]              
                        [0 1 3] x_1 + [0]              
                        [0 0 1]       [2]              
          p(a__zeros) = [1]                            
                        [2]                            
                        [2]                            
               p(adx) = [1 2 0]       [0]              
                        [0 1 2] x_1 + [0]              
                        [0 0 1]       [1]              
              p(cons) = [1 4 2]       [1 1 0]       [0]
                        [0 1 1] x_1 + [0 1 1] x_2 + [1]
                        [0 0 1]       [0 0 1]       [1]
                p(hd) = [1 1 0]       [3]              
                        [0 1 3] x_1 + [1]              
                        [0 0 1]       [2]              
              p(incr) = [1 0 0]       [0]              
                        [0 1 0] x_1 + [1]              
                        [0 0 1]       [0]              
              p(mark) = [1 4 2]       [4]              
                        [0 1 4] x_1 + [0]              
                        [0 0 1]       [2]              
              p(nats) = [0]                            
                        [2]                            
                        [1]                            
                 p(s) = [1 0 0]       [0]              
                        [0 1 0] x_1 + [0]              
                        [0 0 0]       [0]              
                p(tl) = [1 3 0]       [1]              
                        [0 1 3] x_1 + [0]              
                        [0 0 1]       [2]              
             p(zeros) = [0]                            
                        [0]                            
                        [1]                            
        
        Following rules are strictly oriented:
                 a__adx(X) = [1 2 0]     [1]               
                             [0 1 2] X + [0]               
                             [0 0 1]     [1]               
                           > [1 2 0]     [0]               
                             [0 1 2] X + [0]               
                             [0 0 1]     [1]               
                           = adx(X)                        
        
         a__adx(cons(X,Y)) = [1 6 4]     [1 3 2]     [3]   
                             [0 1 3] X + [0 1 3] Y + [3]   
                             [0 0 1]     [0 0 1]     [2]   
                           > [1 4 2]     [1 3 2]     [2]   
                             [0 1 1] X + [0 1 3] Y + [3]   
                             [0 0 1]     [0 0 1]     [2]   
                           = a__incr(cons(X,adx(Y)))       
        
                  a__hd(X) = [1 1 0]     [4]               
                             [0 1 3] X + [1]               
                             [0 0 1]     [2]               
                           > [1 1 0]     [3]               
                             [0 1 3] X + [1]               
                             [0 0 1]     [2]               
                           = hd(X)                         
        
          a__hd(cons(X,Y)) = [1 5 3]     [1 2 1]     [5]   
                             [0 1 4] X + [0 1 4] Y + [5]   
                             [0 0 1]     [0 0 1]     [3]   
                           > [1 4 2]     [4]               
                             [0 1 4] X + [0]               
                             [0 0 1]     [2]               
                           = mark(X)                       
        
                a__incr(X) = [1 0 0]     [2]               
                             [0 1 0] X + [1]               
                             [0 0 1]     [0]               
                           > [1 0 0]     [0]               
                             [0 1 0] X + [1]               
                             [0 0 1]     [0]               
                           = incr(X)                       
        
        a__incr(cons(X,Y)) = [1 4 2]     [1 1 0]     [2]   
                             [0 1 1] X + [0 1 1] Y + [2]   
                             [0 0 1]     [0 0 1]     [1]   
                           > [1 4 0]     [1 1 0]     [1]   
                             [0 1 0] X + [0 1 1] Y + [2]   
                             [0 0 0]     [0 0 1]     [1]   
                           = cons(s(X),incr(Y))            
        
                 a__nats() = [7]                           
                             [6]                           
                             [3]                           
                           > [6]                           
                             [6]                           
                             [3]                           
                           = a__adx(a__zeros())            
        
                 a__nats() = [7]                           
                             [6]                           
                             [3]                           
                           > [0]                           
                             [2]                           
                             [1]                           
                           = nats()                        
        
                  a__tl(X) = [1 3 0]     [4]               
                             [0 1 3] X + [0]               
                             [0 0 1]     [2]               
                           > [1 3 0]     [1]               
                             [0 1 3] X + [0]               
                             [0 0 1]     [2]               
                           = tl(X)                         
        
          a__tl(cons(X,Y)) = [1 7 5]     [1 4 3]     [7]   
                             [0 1 4] X + [0 1 4] Y + [4]   
                             [0 0 1]     [0 0 1]     [3]   
                           > [1 4 2]     [4]               
                             [0 1 4] Y + [0]               
                             [0 0 1]     [2]               
                           = mark(Y)                       
        
                a__zeros() = [1]                           
                             [2]                           
                             [2]                           
                           > [0]                           
                             [2]                           
                             [2]                           
                           = cons(0(),zeros())             
        
                a__zeros() = [1]                           
                             [2]                           
                             [2]                           
                           > [0]                           
                             [0]                           
                             [1]                           
                           = zeros()                       
        
                 mark(0()) = [4]                           
                             [0]                           
                             [2]                           
                           > [0]                           
                             [0]                           
                             [0]                           
                           = 0()                           
        
              mark(adx(X)) = [1 6 10]     [6]              
                             [0 1  6] X + [4]              
                             [0 0  1]     [3]              
                           > [1 6 10]     [5]              
                             [0 1  6] X + [4]              
                             [0 0  1]     [3]              
                           = a__adx(mark(X))               
        
         mark(cons(X1,X2)) = [1 8 8]      [1 5 6]      [10]
                             [0 1 5] X1 + [0 1 5] X2 + [5] 
                             [0 0 1]      [0 0 1]      [3] 
                           > [1 4 2]      [1 1 0]      [0] 
                             [0 1 1] X1 + [0 1 1] X2 + [1] 
                             [0 0 1]      [0 0 1]      [1] 
                           = cons(X1,X2)                   
        
               mark(hd(X)) = [1 5 14]     [15]             
                             [0 1  7] X + [9]              
                             [0 0  1]     [4]              
                           > [1 5 6]     [8]               
                             [0 1 7] X + [7]               
                             [0 0 1]     [4]               
                           = a__hd(mark(X))                
        
             mark(incr(X)) = [1 4 2]     [8]               
                             [0 1 4] X + [1]               
                             [0 0 1]     [2]               
                           > [1 4 2]     [6]               
                             [0 1 4] X + [1]               
                             [0 0 1]     [2]               
                           = a__incr(mark(X))              
        
              mark(nats()) = [14]                          
                             [6]                           
                             [3]                           
                           > [7]                           
                             [6]                           
                             [3]                           
                           = a__nats()                     
        
                mark(s(X)) = [1 4 0]     [4]               
                             [0 1 0] X + [0]               
                             [0 0 0]     [2]               
                           > [1 0 0]     [0]               
                             [0 1 0] X + [0]               
                             [0 0 0]     [0]               
                           = s(X)                          
        
               mark(tl(X)) = [1 7 14]     [9]              
                             [0 1  7] X + [8]              
                             [0 0  1]     [4]              
                           > [1 7 14]     [8]              
                             [0 1  7] X + [6]              
                             [0 0  1]     [4]              
                           = a__tl(mark(X))                
        
             mark(zeros()) = [6]                           
                             [4]                           
                             [3]                           
                           > [1]                           
                             [2]                           
                             [2]                           
                           = a__zeros()                    
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^3))