MAYBE
MAYBE
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)
 }
 DUP: We consider a duplicating system.
  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)
   }
  Fail