YES
Time: 0.001786
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)}
  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))}
   SCCS (4):
    Scc:
     {max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
    Scc:
     {mem#(g(x, y), z) -> mem#(x, z)}
    Scc:
     {++#(x, g(y, z)) -> ++#(x, y)}
    Scc:
     {f#(x, g(y, z)) -> f#(x, y)}
    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)}
     SPSC:
      Simple Projection:
       pi(max#) = 0
      Strict:
       {}
      Qed
    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)}
     SPSC:
      Simple Projection:
       pi(mem#) = 0
      Strict:
       {}
      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)}
     SPSC:
      Simple Projection:
       pi(++#) = 1
      Strict:
       {}
      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)}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {}
      Qed