* Step 1: WeightGap 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:
             runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
            ,true,u}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(++) = [2] x1 + [12] x2 + [1]
                p(=) = [10]                  
                p(f) = [1] x1 + [12] x2 + [0]
            p(false) = [0]                   
                p(g) = [1] x1 + [1] x2 + [0] 
              p(max) = [1] x1 + [0]          
             p(max') = [1] x1 + [1] x2 + [0] 
              p(mem) = [0]                   
              p(nil) = [0]                   
              p(not) = [1] x1 + [1]          
             p(null) = [0]                   
               p(or) = [1] x1 + [1] x2 + [0] 
             p(true) = [0]                   
                p(u) = [0]                   
          
          Following rules are strictly oriented:
          ++(x,nil()) = [2] x + [1]
                      > [1] x + [0]
                      = x          
          
          
          Following rules are (at-least) weakly oriented:
                     ++(x,g(y,z)) =  [2] x + [12] y + [12] z + [1]
                                  >= [2] x + [12] y + [1] z + [1] 
                                  =  g(++(x,y),z)                 
          
                      f(x,g(y,z)) =  [1] x + [12] y + [12] z + [0]
                                  >= [1] x + [12] y + [1] z + [0] 
                                  =  g(f(x,y),z)                  
          
                       f(x,nil()) =  [1] x + [0]                  
                                  >= [1] x + [0]                  
                                  =  g(nil(),x)                   
          
          max(g(g(g(x,y),z),u())) =  [1] x + [1] y + [1] z + [0]  
                                  >= [1] x + [1] y + [1] z + [0]  
                                  =  max'(max(g(g(x,y),z)),u())   
          
             max(g(g(nil(),x),y)) =  [1] x + [1] y + [0]          
                                  >= [1] x + [1] y + [0]          
                                  =  max'(x,y)                    
          
                    mem(x,max(x)) =  [0]                          
                                  >= [1]                          
                                  =  not(null(x))                 
          
                    mem(g(x,y),z) =  [0]                          
                                  >= [10]                         
                                  =  or(=(y,z),mem(x,z))          
          
                     mem(nil(),y) =  [0]                          
                                  >= [0]                          
                                  =  false()                      
          
                     null(g(x,y)) =  [0]                          
                                  >= [0]                          
                                  =  false()                      
          
                      null(nil()) =  [0]                          
                                  >= [0]                          
                                  =  true()                       
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            ++(x,g(y,z)) -> g(++(x,y),z)
            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()
        - Weak TRS:
            ++(x,nil()) -> x
        - 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:
             runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
            ,true,u}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(++) = [4] x1 + [1] x2 + [0]
                p(=) = [0]                  
                p(f) = [1] x1 + [1] x2 + [5]
            p(false) = [0]                  
                p(g) = [1] x1 + [1] x2 + [2]
              p(max) = [1] x1 + [3]         
             p(max') = [1] x1 + [0]         
              p(mem) = [0]                  
              p(nil) = [0]                  
              p(not) = [1] x1 + [0]         
             p(null) = [3]                  
               p(or) = [1] x1 + [1] x2 + [0]
             p(true) = [0]                  
                p(u) = [0]                  
          
          Following rules are strictly oriented:
                       f(x,nil()) = [1] x + [5]                
                                  > [1] x + [2]                
                                  = g(nil(),x)                 
          
          max(g(g(g(x,y),z),u())) = [1] x + [1] y + [1] z + [9]
                                  > [1] x + [1] y + [1] z + [7]
                                  = max'(max(g(g(x,y),z)),u()) 
          
             max(g(g(nil(),x),y)) = [1] x + [1] y + [7]        
                                  > [1] x + [0]                
                                  = max'(x,y)                  
          
                     null(g(x,y)) = [3]                        
                                  > [0]                        
                                  = false()                    
          
                      null(nil()) = [3]                        
                                  > [0]                        
                                  = true()                     
          
          
          Following rules are (at-least) weakly oriented:
           ++(x,g(y,z)) =  [4] x + [1] y + [1] z + [2]
                        >= [4] x + [1] y + [1] z + [2]
                        =  g(++(x,y),z)               
          
            ++(x,nil()) =  [4] x + [0]                
                        >= [1] x + [0]                
                        =  x                          
          
            f(x,g(y,z)) =  [1] x + [1] y + [1] z + [7]
                        >= [1] x + [1] y + [1] z + [7]
                        =  g(f(x,y),z)                
          
          mem(x,max(x)) =  [0]                        
                        >= [3]                        
                        =  not(null(x))               
          
          mem(g(x,y),z) =  [0]                        
                        >= [0]                        
                        =  or(=(y,z),mem(x,z))        
          
           mem(nil(),y) =  [0]                        
                        >= [0]                        
                        =  false()                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            ++(x,g(y,z)) -> g(++(x,y),z)
            f(x,g(y,z)) -> g(f(x,y),z)
            mem(x,max(x)) -> not(null(x))
            mem(g(x,y),z) -> or(=(y,z),mem(x,z))
            mem(nil(),y) -> false()
        - Weak TRS:
            ++(x,nil()) -> x
            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)
            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:
             runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
            ,true,u}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(++) = [1] x1 + [3] x2 + [5]
                p(=) = [0]                  
                p(f) = [4] x1 + [2] x2 + [0]
            p(false) = [2]                  
                p(g) = [1] x1 + [1] x2 + [2]
              p(max) = [2] x1 + [0]         
             p(max') = [1] x1 + [1]         
              p(mem) = [2] x1 + [0]         
              p(nil) = [3]                  
              p(not) = [1] x1 + [4]         
             p(null) = [2]                  
               p(or) = [1] x2 + [0]         
             p(true) = [1]                  
                p(u) = [1]                  
          
          Following rules are strictly oriented:
           ++(x,g(y,z)) = [1] x + [3] y + [3] z + [11]
                        > [1] x + [3] y + [1] z + [7] 
                        = g(++(x,y),z)                
          
            f(x,g(y,z)) = [4] x + [2] y + [2] z + [4] 
                        > [4] x + [2] y + [1] z + [2] 
                        = g(f(x,y),z)                 
          
          mem(g(x,y),z) = [2] x + [2] y + [4]         
                        > [2] x + [0]                 
                        = or(=(y,z),mem(x,z))         
          
           mem(nil(),y) = [6]                         
                        > [2]                         
                        = false()                     
          
          
          Following rules are (at-least) weakly oriented:
                      ++(x,nil()) =  [1] x + [14]                
                                  >= [1] x + [0]                 
                                  =  x                           
          
                       f(x,nil()) =  [4] x + [6]                 
                                  >= [1] x + [5]                 
                                  =  g(nil(),x)                  
          
          max(g(g(g(x,y),z),u())) =  [2] x + [2] y + [2] z + [14]
                                  >= [2] x + [2] y + [2] z + [9] 
                                  =  max'(max(g(g(x,y),z)),u())  
          
             max(g(g(nil(),x),y)) =  [2] x + [2] y + [14]        
                                  >= [1] x + [1]                 
                                  =  max'(x,y)                   
          
                    mem(x,max(x)) =  [2] x + [0]                 
                                  >= [6]                         
                                  =  not(null(x))                
          
                     null(g(x,y)) =  [2]                         
                                  >= [2]                         
                                  =  false()                     
          
                      null(nil()) =  [2]                         
                                  >= [1]                         
                                  =  true()                      
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,max(x)) -> not(null(x))
        - Weak 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(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:
             runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
            ,true,u}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(++) = [1] x1 + [2] x2 + [1]
                p(=) = [1] x1 + [1] x2 + [0]
                p(f) = [2] x1 + [5] x2 + [4]
            p(false) = [0]                  
                p(g) = [1] x1 + [1] x2 + [2]
              p(max) = [1] x1 + [0]         
             p(max') = [1] x1 + [4]         
              p(mem) = [7] x2 + [5]         
              p(nil) = [1]                  
              p(not) = [1] x1 + [1]         
             p(null) = [3]                  
               p(or) = [1] x2 + [0]         
             p(true) = [3]                  
                p(u) = [2]                  
          
          Following rules are strictly oriented:
          mem(x,max(x)) = [7] x + [5] 
                        > [4]         
                        = not(null(x))
          
          
          Following rules are (at-least) weakly oriented:
                     ++(x,g(y,z)) =  [1] x + [2] y + [2] z + [5] 
                                  >= [1] x + [2] y + [1] z + [3] 
                                  =  g(++(x,y),z)                
          
                      ++(x,nil()) =  [1] x + [3]                 
                                  >= [1] x + [0]                 
                                  =  x                           
          
                      f(x,g(y,z)) =  [2] x + [5] y + [5] z + [14]
                                  >= [2] x + [5] y + [1] z + [6] 
                                  =  g(f(x,y),z)                 
          
                       f(x,nil()) =  [2] x + [9]                 
                                  >= [1] x + [3]                 
                                  =  g(nil(),x)                  
          
          max(g(g(g(x,y),z),u())) =  [1] x + [1] y + [1] z + [8] 
                                  >= [1] x + [1] y + [1] z + [8] 
                                  =  max'(max(g(g(x,y),z)),u())  
          
             max(g(g(nil(),x),y)) =  [1] x + [1] y + [5]         
                                  >= [1] x + [4]                 
                                  =  max'(x,y)                   
          
                    mem(g(x,y),z) =  [7] z + [5]                 
                                  >= [7] z + [5]                 
                                  =  or(=(y,z),mem(x,z))         
          
                     mem(nil(),y) =  [7] y + [5]                 
                                  >= [0]                         
                                  =  false()                     
          
                     null(g(x,y)) =  [3]                         
                                  >= [0]                         
                                  =  false()                     
          
                      null(nil()) =  [3]                         
                                  >= [3]                         
                                  =  true()                      
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak 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:
             runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
            ,true,u}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))