Consider the TRS R consisting of the rewrite rules

1: f(x,nil) -> g(nil,x)
2: f(x,g(y,z)) -> g(f(x,y),z)
3: x ++ nil -> x
4: x ++ g(y,z) -> g(x ++ y,z)
5: null(nil) -> true
6: null(g(x,y)) -> false
7: mem(nil,y) -> false
8: mem(g(x,y),z) -> or(y = z,mem(x,z))
9: mem(x,max(x)) -> not(null(x))
10: max(g(g(nil,x),y)) -> max'(x,y)
11: max(g(g(g(x,y),z),u)) -> max'(max(g(g(x,y),z)),u)

There are 5 dependency pairs:

12: F(x,g(y,z)) -> F(x,y)
13: x ++# g(y,z) -> x ++# y
14: MEM(g(x,y),z) -> MEM(x,z)
15: MEM(x,max(x)) -> NULL(x)
16: MAX(g(g(g(x,y),z),u)) -> MAX(g(g(x,y),z))

The approximated dependency graph contains 4 SCCs:
{13},
{12},
{16}
and {14}.

- Consider the SCC {13}.
There are no usable rules.
By taking the polynomial interpretation
[++#](x,y) = [g](x,y) = x + y + 1,
rule 13
is strictly decreasing.

- Consider the SCC {12}.
There are no usable rules.
By taking the polynomial interpretation
[F](x,y) = [g](x,y) = x + y + 1,
rule 12
is strictly decreasing.

- Consider the SCC {16}.
There are no usable rules.
By taking the polynomial interpretation
[u] = 1,
[MAX](x) = x + 1
and [g](x,y) = x + y + 1,
rule 16
is strictly decreasing.

- Consider the SCC {14}.
There are no usable rules.
By taking the polynomial interpretation
[g](x,y) = [MEM](x,y) = x + y + 1,
rule 14
is strictly decreasing.

Hence the TRS is terminating.