Consider the TRS R consisting of the rewrite rules

1: fib(0) -> 0
2: fib(s(0)) -> s(0)
3: fib(s(s(x))) -> fib(s(x)) + fib(x)

There are 2 dependency pairs:

4: FIB(s(s(x))) -> FIB(s(x))
5: FIB(s(s(x))) -> FIB(x)

The approximated dependency graph contains one SCC:
{4,5}.

- Consider the SCC {4,5}.
There are no usable rules.
By taking the polynomial interpretation
[FIB](x) = [s](x) = x + 1,
the rules in {4,5}
are strictly decreasing.

Hence the TRS is terminating.