Consider the TRS R consisting of the rewrite rules
1: f(1) -> f(g(1))
2: f(f(x)) -> f(x)
3: g(0) -> g(f(0))
4: g(g(x)) -> g(x)
There are 4 dependency pairs:
5: F(1) -> F(g(1))
6: F(1) -> G(1)
7: G(0) -> G(f(0))
8: G(0) -> F(0)
The approximated dependency graph contains 2 SCCs:
{5}
and {7}.
- Consider the SCC {5}.
By taking the polynomial interpretation
[g](x) = 0,
[0] = [1] = 1
and [f](x) = [F](x) = x + 1,
the rules in {3,4}
are weakly decreasing and
the rules in {1,2,5}
are strictly decreasing.
- Consider the SCC {7}.
By taking the polynomial interpretation
[f](x) = 0,
[0] = [1] = 1
and [g](x) = [G](x) = x + 1,
the rules in {1,2}
are weakly decreasing and
the rules in {3,4,7}
are strictly decreasing.
Hence the TRS is terminating.