Consider the TRS R consisting of the rewrite rule
1: f(g(x),y,y) -> g(f(x,x,y))
There is one dependency pair:
2: F(g(x),y,y) -> F(x,x,y)
The approximated dependency graph contains one SCC:
{2}.
- Consider the SCC {2}.
There are no usable rules.
By taking the polynomial interpretation
[g](x) = x + 1
and [F](x,y,z) = x + z + 1,
rule 2
is strictly decreasing.
Hence the TRS is terminating.