YES

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())

linear polynomial interpretations on N:

  f_A(x1,x2) = x1 + x2 + 1
  f#_A(x1,x2) = x1 + 7
  nil_A = 2
  nil#_A = 6
  g_A(x1,x2) = x1 + x2 + 1
  g#_A(x1,x2) = 4
  ++_A(x1,x2) = x1 + x2 + 1
  ++#_A(x1,x2) = x1 + x2 + 4
  null_A(x1) = x1 + 1
  null#_A(x1) = 4
  true_A = 0
  true#_A = 5
  false_A = 0
  false#_A = 3
  mem_A(x1,x2) = 1
  mem#_A(x1,x2) = x1 + x2
  or_A(x1,x2) = 0
  or#_A(x1,x2) = 0
  =_A(x1,x2) = x1 + 1
  =#_A(x1,x2) = 0
  max_A(x1) = 5
  max#_A(x1) = x1 + 1
  not_A(x1) = 0
  not#_A(x1) = x1 + 1
  max'_A(x1,x2) = 0
  max'#_A(x1,x2) = 5
  u_A = 2
  u#_A = 0

precedence:

  f > nil = g = ++ > true = mem = or = max > null = = = not = max' = u > false