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())
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [max#](x0) = 4x0,
    
    [mem#](x0, x1) = 2x0 + 2x1 + 6,
    
    [null#](x0) = 0,
    
    [++#](x0, x1) = x1 + 1,
    
    [f#](x0, x1) = 2x1,
    
    [u] = 1,
    
    [max'](x0, x1) = x0 + x1 + 1,
    
    [not](x0) = 0,
    
    [max](x0) = x0 + 2,
    
    [or](x0, x1) = x0 + 2,
    
    [=](x0, x1) = 4x1 + 2,
    
    [mem](x0, x1) = 4x1 + 4,
    
    [false] = 0,
    
    [true] = 2,
    
    [null](x0) = 2,
    
    [++](x0, x1) = 2x0 + 4x1 + 4,
    
    [g](x0, x1) = x0 + x1 + 1,
    
    [f](x0, x1) = x0 + x1 + 5,
    
    [nil] = 0
   orientation:
    f#(x,g(y,z)) = 2y + 2z + 2 >= 2y = f#(x,y)
    
    ++#(x,g(y,z)) = y + z + 2 >= y + 1 = ++#(x,y)
    
    mem#(g(x,y),z) = 2x + 2y + 2z + 8 >= 2x + 2z + 6 = mem#(x,z)
    
    mem#(x,max(x)) = 4x + 10 >= 0 = null#(x)
    
    max#(g(g(g(x,y),z),u())) = 4x + 4y + 4z + 16 >= 4x + 4y + 4z + 8 = max#(g(g(x,y),z))
    
    f(x,nil()) = x + 5 >= x + 1 = g(nil(),x)
    
    f(x,g(y,z)) = x + y + z + 6 >= x + y + z + 6 = g(f(x,y),z)
    
    ++(x,nil()) = 2x + 4 >= x = x
    
    ++(x,g(y,z)) = 2x + 4y + 4z + 8 >= 2x + 4y + z + 5 = g(++(x,y),z)
    
    null(nil()) = 2 >= 2 = true()
    
    null(g(x,y)) = 2 >= 0 = false()
    
    mem(nil(),y) = 4y + 4 >= 0 = false()
    
    mem(g(x,y),z) = 4z + 4 >= 4z + 4 = or(=(y,z),mem(x,z))
    
    mem(x,max(x)) = 4x + 12 >= 0 = not(null(x))
    
    max(g(g(nil(),x),y)) = x + y + 4 >= x + y + 1 = max'(x,y)
    
    max(g(g(g(x,y),z),u())) = x + y + z + 6 >= x + y + z + 6 = max'(max(g(g(x,y),z)),u())
   problem:
    DPs:
     
    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())
   Qed