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

max/plus interpretations on N:

  f_A(x1,x2) = max{0, x1, x2}
  f#_A(x1,x2) = max{0, x1, x2}
  nil_A = 0
  nil#_A = 0
  g_A(x1,x2) = max{0, x1, x2}
  g#_A(x1,x2) = max{0, x1, x2}
  ++_A(x1,x2) = max{0, x1, x2}
  ++#_A(x1,x2) = max{0, x1, x2}
  null_A(x1) = max{0, x1}
  null#_A(x1) = max{0, x1}
  true_A = 0
  true#_A = 0
  false_A = 0
  false#_A = 0
  mem_A(x1,x2) = max{0, x1, x2}
  mem#_A(x1,x2) = max{0, x1, x2}
  or_A(x1,x2) = max{0, x1, x2}
  or#_A(x1,x2) = max{0, x1, x2}
  =_A(x1,x2) = max{0, x1, x2}
  =#_A(x1,x2) = max{0, x1, x2}
  max_A(x1) = max{0, x1}
  max#_A(x1) = max{0, x1}
  not_A(x1) = max{0, x1}
  not#_A(x1) = max{0, x1}
  max'_A(x1,x2) = max{0, x1, x2}
  max'#_A(x1,x2) = max{0, x1, x2}
  u_A = 0
  u#_A = 0

precedence:

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