Consider the TRS R consisting of the rewrite rules 1: fib(0) -> 0 2: fib(s(0)) -> s(0) 3: fib(s(s(0))) -> s(0) 4: fib(s(s(x))) -> sp(g(x)) 5: g(0) -> pair(s(0),0) 6: g(s(0)) -> pair(s(0),s(0)) 7: g(s(x)) -> np(g(x)) 8: sp(pair(x,y)) -> x + y 9: np(pair(x,y)) -> pair(x + y,x) 10: x + 0 -> x 11: x + s(y) -> s(x + y) There are 7 dependency pairs: 12: FIB(s(s(x))) -> SP(g(x)) 13: FIB(s(s(x))) -> G(x) 14: G(s(x)) -> NP(g(x)) 15: G(s(x)) -> G(x) 16: SP(pair(x,y)) -> x +# y 17: NP(pair(x,y)) -> x +# y 18: x +# s(y) -> x +# y The approximated dependency graph contains 2 SCCs: {18} and {15}. - Consider the SCC {18}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [+#](x,y) = x + y + 1, rule 18 is strictly decreasing. - Consider the SCC {15}. There are no usable rules. By taking the polynomial interpretation [G](x) = [s](x) = x + 1, rule 15 is strictly decreasing. Hence the TRS is terminating.