YES

Problem:
 f(x,nil()) -> g(nil(),x)
 f(x,g(y,z)) -> g(f(x,y),z)
 ++(x,nil()) -> x
 ++(x,g(y,z)) -> g(++(x,y),z)
 null(nil()) -> true()
 null(g(x,y)) -> false()
 mem(nil(),y) -> false()
 mem(g(x,y),z) -> or(=(y,z),mem(x,z))
 mem(x,max(x)) -> not(null(x))
 max(g(g(nil(),x),y)) -> max'(x,y)
 max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())

Proof:
 DP Processor:
  DPs:
   f#(x,g(y,z)) -> f#(x,y)
   ++#(x,g(y,z)) -> ++#(x,y)
   mem#(g(x,y),z) -> mem#(x,z)
   mem#(x,max(x)) -> null#(x)
   max#(g(g(g(x,y),z),u())) -> max#(g(g(x,y),z))
  TRS:
   f(x,nil()) -> g(nil(),x)
   f(x,g(y,z)) -> g(f(x,y),z)
   ++(x,nil()) -> x
   ++(x,g(y,z)) -> g(++(x,y),z)
   null(nil()) -> true()
   null(g(x,y)) -> false()
   mem(nil(),y) -> false()
   mem(g(x,y),z) -> or(=(y,z),mem(x,z))
   mem(x,max(x)) -> not(null(x))
   max(g(g(nil(),x),y)) -> max'(x,y)
   max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
  Usable Rule Processor:
   DPs:
    f#(x,g(y,z)) -> f#(x,y)
    ++#(x,g(y,z)) -> ++#(x,y)
    mem#(g(x,y),z) -> mem#(x,z)
    mem#(x,max(x)) -> null#(x)
    max#(g(g(g(x,y),z),u())) -> max#(g(g(x,y),z))
   TRS:
    
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     
    interpretation:
     [max#](x0) = x0,
     
     [mem#](x0, x1) = 4x0 + 1,
     
     [null#](x0) = 4x0,
     
     [++#](x0, x1) = 6x1 + 4,
     
     [f#](x0, x1) = 4x1,
     
     [u] = 2,
     
     [max](x0) = 0,
     
     [g](x0, x1) = x0 + 5x1 + 2
    orientation:
     f#(x,g(y,z)) = 4y + 20z + 8 >= 4y = f#(x,y)
     
     ++#(x,g(y,z)) = 6y + 30z + 16 >= 6y + 4 = ++#(x,y)
     
     mem#(g(x,y),z) = 4x + 20y + 9 >= 4x + 1 = mem#(x,z)
     
     mem#(x,max(x)) = 4x + 1 >= 4x = null#(x)
     
     max#(g(g(g(x,y),z),u())) = x + 5y + 5z + 16 >= x + 5y + 5z + 4 = max#(g(g(x,y),z))
    problem:
     DPs:
      
     TRS:
      
    Qed