Consider the TRS R consisting of the rewrite rules

1: flatten(nil) -> nil
2: flatten(unit(x)) -> flatten(x)
3: flatten(x ++ y) -> flatten(x) ++ flatten(y)
4: flatten(unit(x) ++ y) -> flatten(x) ++ flatten(y)
5: flatten(flatten(x)) -> flatten(x)
6: rev(nil) -> nil
7: rev(unit(x)) -> unit(x)
8: rev(x ++ y) -> rev(y) ++ rev(x)
9: rev(rev(x)) -> x
10: x ++ nil -> x
11: nil ++ y -> y
12: (x ++ y) ++ z -> x ++ (y ++ z)

There are 12 dependency pairs:

13: FLATTEN(unit(x)) -> FLATTEN(x)
14: FLATTEN(x ++ y) -> flatten(x) ++# flatten(y)
15: FLATTEN(x ++ y) -> FLATTEN(x)
16: FLATTEN(x ++ y) -> FLATTEN(y)
17: FLATTEN(unit(x) ++ y) -> flatten(x) ++# flatten(y)
18: FLATTEN(unit(x) ++ y) -> FLATTEN(x)
19: FLATTEN(unit(x) ++ y) -> FLATTEN(y)
20: REV(x ++ y) -> rev(y) ++# rev(x)
21: REV(x ++ y) -> REV(y)
22: REV(x ++ y) -> REV(x)
23: (x ++ y) ++# z -> x ++# (y ++ z)
24: (x ++ y) ++# z -> y ++# z

The approximated dependency graph contains 3 SCCs:
{23,24},
{13,15,16,18,19}
and {21,22}.

- Consider the SCC {23,24}.
The usable rules are {10-12}.
By taking the polynomial interpretation
[nil] = 1
and [++](x,y) = [++#](x,y) = x + y + 1,
the rules in {12,23}
are weakly decreasing and
the rules in {10,11,24}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {23}.
By taking the polynomial interpretation
[nil] = 1,
[++#](x,y) = x + 1
and [++](x,y) = x + y + 1,
rule 12
is weakly decreasing and
the rules in {10,11,23}
are strictly decreasing.


- Consider the SCC {13,15,16,18,19}.
There are no usable rules.
By taking the polynomial interpretation
[FLATTEN](x) = [unit](x) = x + 1
and [++](x,y) = x + y + 1,
the rules in {13,15,16,18,19}
are strictly decreasing.

- Consider the SCC {21,22}.
There are no usable rules.
By taking the polynomial interpretation
[REV](x) = x + 1
and [++](x,y) = x + y + 1,
the rules in {21,22}
are strictly decreasing.

Hence the TRS is terminating.