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)
4: x + 0 -> x
5: x + s(y) -> s(x + y)

There are 4 dependency pairs:

6: FIB(s(s(x))) -> fib(s(x)) +# fib(x)
7: FIB(s(s(x))) -> FIB(s(x))
8: FIB(s(s(x))) -> FIB(x)
9: x +# s(y) -> x +# y

The approximated dependency graph contains 2 SCCs:
{9}
and {7,8}.

- Consider the SCC {9}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [+#](x,y) = x + y + 1,
rule 9
is strictly decreasing.

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

Hence the TRS is terminating.