WORST_CASE(?,O(n^1))
* Step 1: NaturalMI 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:
        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(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(++) = [1] x1 + [3] x2 + [0] 
              p(=) = [1] x2 + [2]          
              p(f) = [2] x1 + [8] x2 + [15]
          p(false) = [0]                   
              p(g) = [1] x1 + [1] x2 + [1] 
            p(max) = [1] x1 + [5]          
           p(max') = [1] x1 + [1] x2 + [0] 
            p(mem) = [1] x1 + [1] x2 + [0] 
            p(nil) = [1]                   
            p(not) = [1] x1 + [0]          
           p(null) = [4]                   
             p(or) = [1] x2 + [0]          
           p(true) = [3]                   
              p(u) = [5]                   
        
        Following rules are strictly oriented:
                   ++(x,g(y,z)) = [1] x + [3] y + [3] z + [3] 
                                > [1] x + [3] y + [1] z + [1] 
                                = g(++(x,y),z)                
        
                    ++(x,nil()) = [1] x + [3]                 
                                > [1] x + [0]                 
                                = x                           
        
                    f(x,g(y,z)) = [2] x + [8] y + [8] z + [23]
                                > [2] x + [8] y + [1] z + [16]
                                = g(f(x,y),z)                 
        
                     f(x,nil()) = [2] x + [23]                
                                > [1] x + [2]                 
                                = g(nil(),x)                  
        
        max(g(g(g(x,y),z),u())) = [1] x + [1] y + [1] z + [13]
                                > [1] x + [1] y + [1] z + [12]
                                = max'(max(g(g(x,y),z)),u())  
        
           max(g(g(nil(),x),y)) = [1] x + [1] y + [8]         
                                > [1] x + [1] y + [0]         
                                = max'(x,y)                   
        
                  mem(x,max(x)) = [2] x + [5]                 
                                > [4]                         
                                = not(null(x))                
        
                  mem(g(x,y),z) = [1] x + [1] y + [1] z + [1] 
                                > [1] x + [1] z + [0]         
                                = or(=(y,z),mem(x,z))         
        
                   mem(nil(),y) = [1] y + [1]                 
                                > [0]                         
                                = false()                     
        
                   null(g(x,y)) = [4]                         
                                > [0]                         
                                = false()                     
        
                    null(nil()) = [4]                         
                                > [3]                         
                                = true()                      
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))