Consider the TRS R consisting of the rewrite rules 1: p(s(x)) -> x 2: fact(0) -> s(0) 3: fact(s(x)) -> s(x) * fact(p(s(x))) 4: 0 * y -> 0 5: s(x) * y -> (x * y) + y 6: x + 0 -> x 7: x + s(y) -> s(x + y) There are 6 dependency pairs: 8: FACT(s(x)) -> s(x) *# fact(p(s(x))) 9: FACT(s(x)) -> FACT(p(s(x))) 10: FACT(s(x)) -> P(s(x)) 11: s(x) *# y -> (x * y) +# y 12: s(x) *# y -> x *# y 13: x +# s(y) -> x +# y The approximated dependency graph contains 3 SCCs: {13}, {12} and {9}. - Consider the SCC {13}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [+#](x,y) = x + y + 1, rule 13 is strictly decreasing. - Consider the SCC {12}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [*#](x,y) = x + y + 1, rule 12 is strictly decreasing. - Consider the SCC {9}. The usable rules are {1}. By taking the polynomial interpretation [FACT](x) = x, [s](x) = x + 1 and [p](x) = x - 1, we obtain a quasi-model of the usable rule. Furthermore, dependency pair 9 is strictly decreasing. Hence the TRS is terminating.