WORST_CASE(?,O(n^1))
* Step 1: NaturalPI 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:
        NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        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) = 2 + x1 + 4*x2       
            p(a__and) = 3 + x1 + 4*x2       
          p(a__first) = 6 + x1 + x2         
           p(a__from) = 4 + 4*x1            
             p(a__if) = 5 + x1 + 4*x2 + 4*x3
               p(add) = 1 + x1 + x2         
               p(and) = 2 + x1 + x2         
              p(cons) = 1                   
             p(false) = 3                   
             p(first) = 2 + x1 + x2         
              p(from) = 2 + x1              
                p(if) = 2 + x1 + x2 + x3    
              p(mark) = 4*x1                
               p(nil) = 2                   
                 p(s) = 1                   
              p(true) = 1                   
        
        Following rules are strictly oriented:
                   a__add(X1,X2) = 2 + X1 + 4*X2              
                                 > 1 + X1 + X2                
                                 = add(X1,X2)                 
        
                   a__add(0(),X) = 4 + 4*X                    
                                 > 4*X                        
                                 = mark(X)                    
        
                  a__add(s(X),Y) = 3 + 4*Y                    
                                 > 1                          
                                 = s(add(X,Y))                
        
                   a__and(X1,X2) = 3 + X1 + 4*X2              
                                 > 2 + X1 + X2                
                                 = and(X1,X2)                 
        
               a__and(false(),Y) = 6 + 4*Y                    
                                 > 3                          
                                 = false()                    
        
                a__and(true(),X) = 4 + 4*X                    
                                 > 4*X                        
                                 = mark(X)                    
        
                 a__first(X1,X2) = 6 + X1 + X2                
                                 > 2 + X1 + X2                
                                 = first(X1,X2)               
        
                 a__first(0(),X) = 8 + X                      
                                 > 2                          
                                 = nil()                      
        
        a__first(s(X),cons(Y,Z)) = 8                          
                                 > 1                          
                                 = cons(Y,first(X,Z))         
        
                      a__from(X) = 4 + 4*X                    
                                 > 1                          
                                 = cons(X,from(s(X)))         
        
                      a__from(X) = 4 + 4*X                    
                                 > 2 + X                      
                                 = from(X)                    
        
                 a__if(X1,X2,X3) = 5 + X1 + 4*X2 + 4*X3       
                                 > 2 + X1 + X2 + X3           
                                 = if(X1,X2,X3)               
        
              a__if(false(),X,Y) = 8 + 4*X + 4*Y              
                                 > 4*Y                        
                                 = mark(Y)                    
        
               a__if(true(),X,Y) = 6 + 4*X + 4*Y              
                                 > 4*X                        
                                 = mark(X)                    
        
                       mark(0()) = 8                          
                                 > 2                          
                                 = 0()                        
        
                mark(add(X1,X2)) = 4 + 4*X1 + 4*X2            
                                 > 2 + 4*X1 + 4*X2            
                                 = a__add(mark(X1),X2)        
        
                mark(and(X1,X2)) = 8 + 4*X1 + 4*X2            
                                 > 3 + 4*X1 + 4*X2            
                                 = a__and(mark(X1),X2)        
        
               mark(cons(X1,X2)) = 4                          
                                 > 1                          
                                 = cons(X1,X2)                
        
                   mark(false()) = 12                         
                                 > 3                          
                                 = false()                    
        
              mark(first(X1,X2)) = 8 + 4*X1 + 4*X2            
                                 > 6 + 4*X1 + 4*X2            
                                 = a__first(mark(X1),mark(X2))
        
                   mark(from(X)) = 8 + 4*X                    
                                 > 4 + 4*X                    
                                 = a__from(X)                 
        
              mark(if(X1,X2,X3)) = 8 + 4*X1 + 4*X2 + 4*X3     
                                 > 5 + 4*X1 + 4*X2 + 4*X3     
                                 = a__if(mark(X1),X2,X3)      
        
                     mark(nil()) = 8                          
                                 > 2                          
                                 = nil()                      
        
                      mark(s(X)) = 4                          
                                 > 1                          
                                 = s(X)                       
        
                    mark(true()) = 4                          
                                 > 1                          
                                 = true()                     
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))