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