Consider the TRS R consisting of the rewrite rules

1: f(nil) -> nil
2: f(nil . y) -> nil . f(y)
3: f((x . y) . z) -> f(x . (y . z))
4: g(nil) -> nil
5: g(x . nil) -> g(x) . nil
6: g(x . (y . z)) -> g((x . y) . z)

There are 4 dependency pairs:

7: F(nil . y) -> F(y)
8: F((x . y) . z) -> F(x . (y . z))
9: G(x . nil) -> G(x)
10: G(x . (y . z)) -> G((x . y) . z)

The approximated dependency graph contains 2 SCCs:
{7,8}
and {9,10}.

- Consider the SCC {7,8}.
There are no usable rules.
By taking the polynomial interpretation
[nil] = 1,
[F](x) = x + 1
and [.](x,y) = x + y + 1,
rule 8
is weakly decreasing and
rule 7
is strictly decreasing.
There is one new SCC.

- Consider the SCC {8}.
By taking the polynomial interpretation
[.](x,y) = [F](x) = x + 1,
rule 8
is strictly decreasing.


- Consider the SCC {9,10}.
There are no usable rules.
By taking the polynomial interpretation
[nil] = 1,
[G](x) = x + 1
and [.](x,y) = x + y + 1,
rule 10
is weakly decreasing and
rule 9
is strictly decreasing.
There is one new SCC.

- Consider the SCC {10}.
By taking the polynomial interpretation
[G](x) = x + 1
and [.](x,y) = y + 1,
rule 10
is strictly decreasing.


Hence the TRS is terminating.