WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            a__add(X1,X2) -> add(X1,X2)
            a__add(0(),X) -> mark(X)
            a__add(s(X),Y) -> s(add(X,Y))
            a__and(X1,X2) -> and(X1,X2)
            a__and(false(),Y) -> false()
            a__and(true(),X) -> mark(X)
            a__first(X1,X2) -> first(X1,X2)
            a__first(0(),X) -> nil()
            a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
            a__from(X) -> cons(X,from(s(X)))
            a__from(X) -> from(X)
            a__if(X1,X2,X3) -> if(X1,X2,X3)
            a__if(false(),X,Y) -> mark(Y)
            a__if(true(),X,Y) -> mark(X)
            mark(0()) -> 0()
            mark(add(X1,X2)) -> a__add(mark(X1),X2)
            mark(and(X1,X2)) -> a__and(mark(X1),X2)
            mark(cons(X1,X2)) -> cons(X1,X2)
            mark(false()) -> false()
            mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
            mark(from(X)) -> a__from(X)
            mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
            mark(nil()) -> nil()
            mark(s(X)) -> s(X)
            mark(true()) -> true()
        - Signature:
            {a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1} / {0/0,add/2,and/2,cons/2,false/0,first/2,from/1
            ,if/3,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__add,a__and,a__first,a__from,a__if
            ,mark} and constructors {0,add,and,cons,false,first,from,if,nil,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__add) = {1},
          uargs(a__and) = {1},
          uargs(a__first) = {1,2},
          uargs(a__if) = {1}
        
        Following symbols are considered usable:
          {a__add,a__and,a__first,a__from,a__if,mark}
        TcT has computed the following interpretation:
                 p(0) = [2]                           
            p(a__add) = [1] x1 + [8] x2 + [9]         
            p(a__and) = [1] x1 + [8] x2 + [10]        
          p(a__first) = [1] x1 + [1] x2 + [3]         
           p(a__from) = [6]                           
             p(a__if) = [1] x1 + [8] x2 + [8] x3 + [9]
               p(add) = [1] x1 + [1] x2 + [3]         
               p(and) = [1] x1 + [1] x2 + [2]         
              p(cons) = [2]                           
             p(false) = [2]                           
             p(first) = [1] x1 + [1] x2 + [2]         
              p(from) = [2]                           
                p(if) = [1] x1 + [1] x2 + [1] x3 + [2]
              p(mark) = [8] x1 + [0]                  
               p(nil) = [1]                           
                 p(s) = [1] x1 + [2]                  
              p(true) = [2]                           
        
        Following rules are strictly oriented:
                   a__add(X1,X2) = [1] X1 + [8] X2 + [9]          
                                 > [1] X1 + [1] X2 + [3]          
                                 = add(X1,X2)                     
        
                   a__add(0(),X) = [8] X + [11]                   
                                 > [8] X + [0]                    
                                 = mark(X)                        
        
                  a__add(s(X),Y) = [1] X + [8] Y + [11]           
                                 > [1] X + [1] Y + [5]            
                                 = s(add(X,Y))                    
        
                   a__and(X1,X2) = [1] X1 + [8] X2 + [10]         
                                 > [1] X1 + [1] X2 + [2]          
                                 = and(X1,X2)                     
        
               a__and(false(),Y) = [8] Y + [12]                   
                                 > [2]                            
                                 = false()                        
        
                a__and(true(),X) = [8] X + [12]                   
                                 > [8] X + [0]                    
                                 = mark(X)                        
        
                 a__first(X1,X2) = [1] X1 + [1] X2 + [3]          
                                 > [1] X1 + [1] X2 + [2]          
                                 = first(X1,X2)                   
        
                 a__first(0(),X) = [1] X + [5]                    
                                 > [1]                            
                                 = nil()                          
        
        a__first(s(X),cons(Y,Z)) = [1] X + [7]                    
                                 > [2]                            
                                 = cons(Y,first(X,Z))             
        
                      a__from(X) = [6]                            
                                 > [2]                            
                                 = cons(X,from(s(X)))             
        
                      a__from(X) = [6]                            
                                 > [2]                            
                                 = from(X)                        
        
                 a__if(X1,X2,X3) = [1] X1 + [8] X2 + [8] X3 + [9] 
                                 > [1] X1 + [1] X2 + [1] X3 + [2] 
                                 = if(X1,X2,X3)                   
        
              a__if(false(),X,Y) = [8] X + [8] Y + [11]           
                                 > [8] Y + [0]                    
                                 = mark(Y)                        
        
               a__if(true(),X,Y) = [8] X + [8] Y + [11]           
                                 > [8] X + [0]                    
                                 = mark(X)                        
        
                       mark(0()) = [16]                           
                                 > [2]                            
                                 = 0()                            
        
                mark(add(X1,X2)) = [8] X1 + [8] X2 + [24]         
                                 > [8] X1 + [8] X2 + [9]          
                                 = a__add(mark(X1),X2)            
        
                mark(and(X1,X2)) = [8] X1 + [8] X2 + [16]         
                                 > [8] X1 + [8] X2 + [10]         
                                 = a__and(mark(X1),X2)            
        
               mark(cons(X1,X2)) = [16]                           
                                 > [2]                            
                                 = cons(X1,X2)                    
        
                   mark(false()) = [16]                           
                                 > [2]                            
                                 = false()                        
        
              mark(first(X1,X2)) = [8] X1 + [8] X2 + [16]         
                                 > [8] X1 + [8] X2 + [3]          
                                 = a__first(mark(X1),mark(X2))    
        
                   mark(from(X)) = [16]                           
                                 > [6]                            
                                 = a__from(X)                     
        
              mark(if(X1,X2,X3)) = [8] X1 + [8] X2 + [8] X3 + [16]
                                 > [8] X1 + [8] X2 + [8] X3 + [9] 
                                 = a__if(mark(X1),X2,X3)          
        
                     mark(nil()) = [8]                            
                                 > [1]                            
                                 = nil()                          
        
                      mark(s(X)) = [8] X + [16]                   
                                 > [1] X + [2]                    
                                 = s(X)                           
        
                    mark(true()) = [16]                           
                                 > [2]                            
                                 = true()                         
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))