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())
  TDG 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())
   graph:
    max#(g(g(g(x,y),z),u())) -> max#(g(g(x,y),z)) ->
    max#(g(g(g(x,y),z),u())) -> max#(g(g(x,y),z))
    mem#(g(x,y),z) -> mem#(x,z) -> mem#(x,max(x)) -> null#(x)
    mem#(g(x,y),z) -> mem#(x,z) -> mem#(g(x,y),z) -> mem#(x,z)
    ++#(x,g(y,z)) -> ++#(x,y) -> ++#(x,g(y,z)) -> ++#(x,y)
    f#(x,g(y,z)) -> f#(x,y) -> f#(x,g(y,z)) -> f#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 4
    #arcs: 5/25
    DPs:
     f#(x,g(y,z)) -> f#(x,y)
    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())
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(f) = [0,1]
      pi(g) = [0]
      pi(++) = [0,1]
      pi(null) = 0
      pi(true) = []
      pi(false) = []
      pi(mem) = 0
      pi(=) = 1
      pi(or) = 1
      pi(max) = []
      pi(not) = 0
      pi(max') = []
      pi(u) = []
      pi(f#) = 1
     weight function:
      w0 = 1
      w(f#) = w(u) = w(max') = w(not) = w(max) = w(or) = w(=) = w(mem) = w(
      false) = w(true) = w(null) = w(g) = w(f) = w(nil) = 1
      w(++) = 0
     precedence:
      f# ~ u ~ max ~ ++ ~ f ~ nil > max' ~ not ~ or ~ = ~ mem ~ false ~ true ~ null ~ g
     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
    
    DPs:
     ++#(x,g(y,z)) -> ++#(x,y)
    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())
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(f) = [0,1]
      pi(g) = [0]
      pi(++) = [0,1]
      pi(null) = 0
      pi(true) = []
      pi(false) = []
      pi(mem) = 0
      pi(=) = 1
      pi(or) = 1
      pi(max) = []
      pi(not) = 0
      pi(max') = []
      pi(u) = []
      pi(++#) = 1
     weight function:
      w0 = 1
      w(++#) = w(u) = w(max') = w(not) = w(max) = w(or) = w(=) = w(mem) = w(
      false) = w(true) = w(null) = w(g) = w(f) = w(nil) = 1
      w(++) = 0
     precedence:
      ++# ~ u ~ max ~ ++ ~ f ~ nil > max' ~ not ~ or ~ = ~ mem ~ false ~ true ~ null ~ g
     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
    
    DPs:
     mem#(g(x,y),z) -> mem#(x,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())
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(f) = [1]
      pi(g) = [0]
      pi(++) = [0,1]
      pi(null) = 0
      pi(true) = []
      pi(false) = []
      pi(mem) = [0]
      pi(=) = 1
      pi(or) = []
      pi(max) = []
      pi(not) = 0
      pi(max') = []
      pi(u) = []
      pi(mem#) = 0
     weight function:
      w0 = 1
      w(mem#) = w(u) = w(max') = w(not) = w(max) = w(or) = w(=) = w(false) = w(
      true) = w(null) = w(g) = w(f) = w(nil) = 1
      w(mem) = w(++) = 0
     precedence:
      not > mem# ~ max ~ or ~ mem ~ ++ ~ f ~ nil > u ~ max' ~ = ~ false ~ true ~ null ~ g
     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
    
    DPs:
     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())
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(f) = [0,1]
      pi(g) = [0]
      pi(++) = [0,1]
      pi(null) = 0
      pi(true) = []
      pi(false) = []
      pi(mem) = 0
      pi(=) = 1
      pi(or) = 1
      pi(max) = 0
      pi(not) = 0
      pi(max') = []
      pi(u) = []
      pi(max#) = 0
     weight function:
      w0 = 1
      w(max#) = w(u) = w(max') = w(max) = w(or) = w(mem) = w(false) = w(
      true) = w(null) = w(g) = w(nil) = 1
      w(not) = w(=) = w(++) = w(f) = 0
     precedence:
      u ~ ++ ~ f ~ nil > max# ~ max' ~ not ~ max ~ or ~ = ~ mem ~ false ~ true ~ null ~ g
     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