WORST_CASE(?,O(n^1))
* Step 1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            ++(x,g(y,z)) -> g(++(x,y),z)
            ++(x,nil()) -> x
            f(x,g(y,z)) -> g(f(x,y),z)
            f(x,nil()) -> g(nil(),x)
            max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
            max(g(g(nil(),x),y)) -> max'(x,y)
            mem(x,max(x)) -> not(null(x))
            mem(g(x,y),z) -> or(=(y,z),mem(x,z))
            mem(nil(),y) -> false()
            null(g(x,y)) -> false()
            null(nil()) -> true()
        - Signature:
            {++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil
            ,not,or,true,u}
    + 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(g) = {1},
          uargs(max') = {1},
          uargs(not) = {1},
          uargs(or) = {2}
        
        Following symbols are considered usable:
          {++,f,max,mem,null}
        TcT has computed the following interpretation:
             p(++) = 4*x1 + 4*x2    
              p(=) = 1              
              p(f) = 2 + 4*x1 + 4*x2
          p(false) = 0              
              p(g) = 1 + x1 + x2    
            p(max) = 1 + 4*x1       
           p(max') = 2 + x1 + x2    
            p(mem) = 6 + 7*x1 + 2*x2
            p(nil) = 1              
            p(not) = 4 + x1         
           p(null) = 2              
             p(or) = 6 + x2         
           p(true) = 1              
              p(u) = 0              
        
        Following rules are strictly oriented:
                   ++(x,g(y,z)) = 4 + 4*x + 4*y + 4*z       
                                > 1 + 4*x + 4*y + z         
                                = g(++(x,y),z)              
        
                    ++(x,nil()) = 4 + 4*x                   
                                > x                         
                                = x                         
        
                    f(x,g(y,z)) = 6 + 4*x + 4*y + 4*z       
                                > 3 + 4*x + 4*y + z         
                                = g(f(x,y),z)               
        
                     f(x,nil()) = 6 + 4*x                   
                                > 2 + x                     
                                = g(nil(),x)                
        
        max(g(g(g(x,y),z),u())) = 13 + 4*x + 4*y + 4*z      
                                > 11 + 4*x + 4*y + 4*z      
                                = max'(max(g(g(x,y),z)),u())
        
           max(g(g(nil(),x),y)) = 13 + 4*x + 4*y            
                                > 2 + x + y                 
                                = max'(x,y)                 
        
                  mem(x,max(x)) = 8 + 15*x                  
                                > 6                         
                                = not(null(x))              
        
                  mem(g(x,y),z) = 13 + 7*x + 7*y + 2*z      
                                > 12 + 7*x + 2*z            
                                = or(=(y,z),mem(x,z))       
        
                   mem(nil(),y) = 13 + 2*y                  
                                > 0                         
                                = false()                   
        
                   null(g(x,y)) = 2                         
                                > 0                         
                                = false()                   
        
                    null(nil()) = 2                         
                                > 1                         
                                = true()                    
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))