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:
    
   ADG 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:
     
    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#(g(x,y),z) -> mem#(x,z)
     mem#(g(x,y),z) -> mem#(x,z) -> mem#(x,max(x)) -> null#(x)
     ++#(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)
    Restore Modifier:
     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())
     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())
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [u] = 0,
        
        [max'](x0, x1) = 0,
        
        [not](x0) = 1,
        
        [max](x0) = 0,
        
        [or](x0, x1) = 1,
        
        [=](x0, x1) = 0,
        
        [mem](x0, x1) = 1,
        
        [false] = 1,
        
        [true] = 0,
        
        [null](x0) = 1,
        
        [++](x0, x1) = x0 + x1 + 1,
        
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x1 + 1,
        
        [nil] = 0
       orientation:
        f#(x,g(y,z)) = y + 1 >= y = f#(x,y)
        
        f(x,nil()) = 1 >= 1 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        ++(x,nil()) = x + 1 >= x = x
        
        ++(x,g(y,z)) = x + y + 2 >= x + y + 2 = g(++(x,y),z)
        
        null(nil()) = 1 >= 0 = true()
        
        null(g(x,y)) = 1 >= 1 = false()
        
        mem(nil(),y) = 1 >= 1 = false()
        
        mem(g(x,y),z) = 1 >= 1 = or(=(y,z),mem(x,z))
        
        mem(x,max(x)) = 1 >= 1 = not(null(x))
        
        max(g(g(nil(),x),y)) = 0 >= 0 = max'(x,y)
        
        max(g(g(g(x,y),z),u())) = 0 >= 0 = 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
      
      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())
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [++#](x0, x1) = x1,
        
        [u] = 0,
        
        [max'](x0, x1) = 0,
        
        [not](x0) = 1,
        
        [max](x0) = 0,
        
        [or](x0, x1) = 1,
        
        [=](x0, x1) = 0,
        
        [mem](x0, x1) = 1,
        
        [false] = 1,
        
        [true] = 0,
        
        [null](x0) = 1,
        
        [++](x0, x1) = x0 + x1 + 1,
        
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x1 + 1,
        
        [nil] = 0
       orientation:
        ++#(x,g(y,z)) = y + 1 >= y = ++#(x,y)
        
        f(x,nil()) = 1 >= 1 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        ++(x,nil()) = x + 1 >= x = x
        
        ++(x,g(y,z)) = x + y + 2 >= x + y + 2 = g(++(x,y),z)
        
        null(nil()) = 1 >= 0 = true()
        
        null(g(x,y)) = 1 >= 1 = false()
        
        mem(nil(),y) = 1 >= 1 = false()
        
        mem(g(x,y),z) = 1 >= 1 = or(=(y,z),mem(x,z))
        
        mem(x,max(x)) = 1 >= 1 = not(null(x))
        
        max(g(g(nil(),x),y)) = 0 >= 0 = max'(x,y)
        
        max(g(g(g(x,y),z),u())) = 0 >= 0 = 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
      
      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())
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [mem#](x0, x1) = x0,
        
        [u] = 0,
        
        [max'](x0, x1) = 0,
        
        [not](x0) = 1,
        
        [max](x0) = 0,
        
        [or](x0, x1) = 1,
        
        [=](x0, x1) = 0,
        
        [mem](x0, x1) = 1,
        
        [false] = 1,
        
        [true] = 0,
        
        [null](x0) = 1,
        
        [++](x0, x1) = x0 + x1 + 1,
        
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x1 + 1,
        
        [nil] = 0
       orientation:
        mem#(g(x,y),z) = x + 1 >= x = mem#(x,z)
        
        f(x,nil()) = 1 >= 1 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        ++(x,nil()) = x + 1 >= x = x
        
        ++(x,g(y,z)) = x + y + 2 >= x + y + 2 = g(++(x,y),z)
        
        null(nil()) = 1 >= 0 = true()
        
        null(g(x,y)) = 1 >= 1 = false()
        
        mem(nil(),y) = 1 >= 1 = false()
        
        mem(g(x,y),z) = 1 >= 1 = or(=(y,z),mem(x,z))
        
        mem(x,max(x)) = 1 >= 1 = not(null(x))
        
        max(g(g(nil(),x),y)) = 0 >= 0 = max'(x,y)
        
        max(g(g(g(x,y),z),u())) = 0 >= 0 = 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
      
      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())
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [max#](x0) = x0,
        
        [u] = 0,
        
        [max'](x0, x1) = 0,
        
        [not](x0) = 0,
        
        [max](x0) = 0,
        
        [or](x0, x1) = 0,
        
        [=](x0, x1) = 0,
        
        [mem](x0, x1) = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [null](x0) = 0,
        
        [++](x0, x1) = x0 + x1,
        
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x1 + 1,
        
        [nil] = 1
       orientation:
        max#(g(g(g(x,y),z),u())) = x + 3 >= x + 2 = max#(g(g(x,y),z))
        
        f(x,nil()) = 2 >= 2 = g(nil(),x)
        
        f(x,g(y,z)) = y + 2 >= y + 2 = g(f(x,y),z)
        
        ++(x,nil()) = x + 1 >= x = x
        
        ++(x,g(y,z)) = x + y + 1 >= x + y + 1 = g(++(x,y),z)
        
        null(nil()) = 0 >= 0 = true()
        
        null(g(x,y)) = 0 >= 0 = false()
        
        mem(nil(),y) = 0 >= 0 = false()
        
        mem(g(x,y),z) = 0 >= 0 = or(=(y,z),mem(x,z))
        
        mem(x,max(x)) = 0 >= 0 = not(null(x))
        
        max(g(g(nil(),x),y)) = 0 >= 0 = max'(x,y)
        
        max(g(g(g(x,y),z),u())) = 0 >= 0 = 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