Consider the TRS R consisting of the rewrite rules

1: fib(N) -> sel(N,fib1(s(0),s(0)))
2: fib1(X,Y) -> cons(X,n__fib1(Y,add(X,Y)))
3: add(0,X) -> X
4: add(s(X),Y) -> s(add(X,Y))
5: sel(0,cons(X,XS)) -> X
6: sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
7: fib1(X1,X2) -> n__fib1(X1,X2)
8: activate(n__fib1(X1,X2)) -> fib1(X1,X2)
9: activate(X) -> X

There are 7 dependency pairs:

10: FIB(N) -> SEL(N,fib1(s(0),s(0)))
11: FIB(N) -> FIB1(s(0),s(0))
12: FIB1(X,Y) -> ADD(X,Y)
13: ADD(s(X),Y) -> ADD(X,Y)
14: SEL(s(N),cons(X,XS)) -> SEL(N,activate(XS))
15: SEL(s(N),cons(X,XS)) -> ACTIVATE(XS)
16: ACTIVATE(n__fib1(X1,X2)) -> FIB1(X1,X2)

The approximated dependency graph contains 2 SCCs:
{13}
and {14}.

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

- Consider the SCC {14}.
The usable rules are {2-4,7-9}.
By taking the polynomial interpretation
[0] = 1,
[activate](x) = [cons](x,y) = [s](x) = [SEL](x,y) = x + 1
and [add](x,y) = [fib1](x,y) = [n__fib1](x,y) = x + y + 1,
the rules in {2,4,7}
are weakly decreasing and
the rules in {3,8,9,14}
are strictly decreasing.

Hence the TRS is terminating.