YES
Time: 0.113474
TRS:
 {            f(x, g(y, z)) -> g(f(x, y), z),
                f(x, nil()) -> g(nil(), x),
             ++(x, g(y, z)) -> g(++(x, y), z),
               ++(x, nil()) -> x,
               null g(x, y) -> false(),
                 null nil() -> true(),
              mem(x, max x) -> not null x,
            mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
              mem(nil(), y) -> false(),
  max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
      max g(g(nil(), x), y) -> max'(x, y)}
 DP:
  DP:
   {            f#(x, g(y, z)) -> f#(x, y),
               ++#(x, g(y, z)) -> ++#(x, y),
                mem#(x, max x) -> null# x,
              mem#(g(x, y), z) -> mem#(x, z),
    max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
  TRS:
  {            f(x, g(y, z)) -> g(f(x, y), z),
                 f(x, nil()) -> g(nil(), x),
              ++(x, g(y, z)) -> g(++(x, y), z),
                ++(x, nil()) -> x,
                null g(x, y) -> false(),
                  null nil() -> true(),
               mem(x, max x) -> not null x,
             mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
               mem(nil(), y) -> false(),
   max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
       max g(g(nil(), x), y) -> max'(x, y)}
  UR:
   {}
   EDG:
    {(++#(x, g(y, z)) -> ++#(x, y), ++#(x, g(y, z)) -> ++#(x, y))
     (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))
     (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))
     (f#(x, g(y, z)) -> f#(x, y), f#(x, g(y, z)) -> f#(x, y))}
    STATUS:
     arrows: 0.800000
     SCCS (4):
      Scc:
       {mem#(g(x, y), z) -> mem#(x, z)}
      Scc:
       {max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
      Scc:
       {++#(x, g(y, z)) -> ++#(x, y)}
      Scc:
       {f#(x, g(y, z)) -> f#(x, y)}
      
      SCC (1):
       Strict:
        {mem#(g(x, y), z) -> mem#(x, z)}
       Weak:
       {            f(x, g(y, z)) -> g(f(x, y), z),
                      f(x, nil()) -> g(nil(), x),
                   ++(x, g(y, z)) -> g(++(x, y), z),
                     ++(x, nil()) -> x,
                     null g(x, y) -> false(),
                       null nil() -> true(),
                    mem(x, max x) -> not null x,
                  mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                    mem(nil(), y) -> false(),
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
            max g(g(nil(), x), y) -> max'(x, y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [g](x0, x1) = x0 + 1,
         
         [f](x0, x1) = x0 + 1,
         
         [++](x0, x1) = x0 + 1,
         
         [mem](x0, x1) = x0 + x1 + 1,
         
         [or](x0, x1) = x0 + x1,
         
         [=](x0, x1) = x0,
         
         [max'](x0, x1) = x0 + x1,
         
         [null](x0) = x0 + 1,
         
         [not](x0) = 0,
         
         [max](x0) = 1,
         
         [nil] = 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [u] = 1,
         
         [mem#](x0, x1) = x0
        Strict:
         mem#(g(x, y), z) -> mem#(x, z)
         1 + 1x + 0y + 0z >= 0 + 1x + 0z
        Weak:
         max g(g(nil(), x), y) -> max'(x, y)
         1 + 0x + 0y >= 0 + 1x + 1y
         max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u())
         1 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z
         mem(nil(), y) -> false()
         2 + 1y >= 0
         mem(g(x, y), z) -> or(=(y, z), mem(x, z))
         2 + 1x + 0y + 1z >= 1 + 1x + 0y + 2z
         mem(x, max x) -> not null x
         2 + 1x >= 0 + 0x
         null nil() -> true()
         2 >= 0
         null g(x, y) -> false()
         2 + 1x + 0y >= 0
         ++(x, nil()) -> x
         2 + 0x >= 1x
         ++(x, g(y, z)) -> g(++(x, y), z)
         2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
         f(x, nil()) -> g(nil(), x)
         2 + 0x >= 2 + 0x
         f(x, g(y, z)) -> g(f(x, y), z)
         2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
       Qed
     
     SCC (1):
      Strict:
       {max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
      Weak:
      {            f(x, g(y, z)) -> g(f(x, y), z),
                     f(x, nil()) -> g(nil(), x),
                  ++(x, g(y, z)) -> g(++(x, y), z),
                    ++(x, nil()) -> x,
                    null g(x, y) -> false(),
                      null nil() -> true(),
                   mem(x, max x) -> not null x,
                 mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                   mem(nil(), y) -> false(),
       max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
           max g(g(nil(), x), y) -> max'(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = x0 + x1,
        
        [f](x0, x1) = 0,
        
        [++](x0, x1) = 0,
        
        [mem](x0, x1) = x0 + x1,
        
        [or](x0, x1) = 0,
        
        [=](x0, x1) = 0,
        
        [max'](x0, x1) = x0 + 1,
        
        [null](x0) = 0,
        
        [not](x0) = 0,
        
        [max](x0) = x0,
        
        [nil] = 0,
        
        [true] = 0,
        
        [false] = 0,
        
        [u] = 1,
        
        [max#](x0) = x0
       Strict:
        max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)
        1 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       Weak:
        max g(g(nil(), x), y) -> max'(x, y)
        0 + 1x + 1y >= 1 + 0x + 1y
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u())
        1 + 1x + 1y + 1z >= 2 + 0x + 0y + 0z
        mem(nil(), y) -> false()
        0 + 1y >= 0
        mem(g(x, y), z) -> or(=(y, z), mem(x, z))
        0 + 1x + 1y + 1z >= 0 + 0x + 0y + 0z
        mem(x, max x) -> not null x
        0 + 2x >= 0 + 0x
        null nil() -> true()
        0 >= 0
        null g(x, y) -> false()
        0 + 0x + 0y >= 0
        ++(x, nil()) -> x
        0 + 0x >= 1x
        ++(x, g(y, z)) -> g(++(x, y), z)
        0 + 0x + 0y + 0z >= 0 + 0x + 0y + 1z
        f(x, nil()) -> g(nil(), x)
        0 + 0x >= 0 + 1x
        f(x, g(y, z)) -> g(f(x, y), z)
        0 + 0x + 0y + 0z >= 0 + 0x + 0y + 1z
      Qed
     SCC (1):
      Strict:
       {++#(x, g(y, z)) -> ++#(x, y)}
      Weak:
      {            f(x, g(y, z)) -> g(f(x, y), z),
                     f(x, nil()) -> g(nil(), x),
                  ++(x, g(y, z)) -> g(++(x, y), z),
                    ++(x, nil()) -> x,
                    null g(x, y) -> false(),
                      null nil() -> true(),
                   mem(x, max x) -> not null x,
                 mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                   mem(nil(), y) -> false(),
       max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
           max g(g(nil(), x), y) -> max'(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x0 + 1,
        
        [++](x0, x1) = x0 + 1,
        
        [mem](x0, x1) = x0 + x1 + 1,
        
        [or](x0, x1) = x0 + x1,
        
        [=](x0, x1) = x0,
        
        [max'](x0, x1) = x0 + x1,
        
        [null](x0) = x0 + 1,
        
        [not](x0) = 0,
        
        [max](x0) = 1,
        
        [nil] = 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [u] = 1,
        
        [++#](x0, x1) = x0
       Strict:
        ++#(x, g(y, z)) -> ++#(x, y)
        1 + 0x + 1y + 0z >= 0 + 0x + 1y
       Weak:
        max g(g(nil(), x), y) -> max'(x, y)
        1 + 0x + 0y >= 0 + 1x + 1y
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u())
        1 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z
        mem(nil(), y) -> false()
        2 + 1y >= 0
        mem(g(x, y), z) -> or(=(y, z), mem(x, z))
        2 + 1x + 0y + 1z >= 1 + 1x + 0y + 2z
        mem(x, max x) -> not null x
        2 + 1x >= 0 + 0x
        null nil() -> true()
        2 >= 0
        null g(x, y) -> false()
        2 + 1x + 0y >= 0
        ++(x, nil()) -> x
        2 + 0x >= 1x
        ++(x, g(y, z)) -> g(++(x, y), z)
        2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
        f(x, nil()) -> g(nil(), x)
        2 + 0x >= 2 + 0x
        f(x, g(y, z)) -> g(f(x, y), z)
        2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
      Qed
    SCC (1):
     Strict:
      {f#(x, g(y, z)) -> f#(x, y)}
     Weak:
     {            f(x, g(y, z)) -> g(f(x, y), z),
                    f(x, nil()) -> g(nil(), x),
                 ++(x, g(y, z)) -> g(++(x, y), z),
                   ++(x, nil()) -> x,
                   null g(x, y) -> false(),
                     null nil() -> true(),
                  mem(x, max x) -> not null x,
                mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                  mem(nil(), y) -> false(),
      max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
          max g(g(nil(), x), y) -> max'(x, y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [g](x0, x1) = x0 + 1,
       
       [f](x0, x1) = x0 + 1,
       
       [++](x0, x1) = x0 + 1,
       
       [mem](x0, x1) = x0 + x1 + 1,
       
       [or](x0, x1) = x0 + x1,
       
       [=](x0, x1) = x0,
       
       [max'](x0, x1) = x0 + x1,
       
       [null](x0) = x0 + 1,
       
       [not](x0) = 0,
       
       [max](x0) = 1,
       
       [nil] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [u] = 1,
       
       [f#](x0, x1) = x0
      Strict:
       f#(x, g(y, z)) -> f#(x, y)
       1 + 0x + 1y + 0z >= 0 + 0x + 1y
      Weak:
       max g(g(nil(), x), y) -> max'(x, y)
       1 + 0x + 0y >= 0 + 1x + 1y
       max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u())
       1 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z
       mem(nil(), y) -> false()
       2 + 1y >= 0
       mem(g(x, y), z) -> or(=(y, z), mem(x, z))
       2 + 1x + 0y + 1z >= 1 + 1x + 0y + 2z
       mem(x, max x) -> not null x
       2 + 1x >= 0 + 0x
       null nil() -> true()
       2 >= 0
       null g(x, y) -> false()
       2 + 1x + 0y >= 0
       ++(x, nil()) -> x
       2 + 0x >= 1x
       ++(x, g(y, z)) -> g(++(x, y), z)
       2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
       f(x, nil()) -> g(nil(), x)
       2 + 0x >= 2 + 0x
       f(x, g(y, z)) -> g(f(x, y), z)
       2 + 0x + 1y + 0z >= 2 + 0x + 1y + 0z
     Qed