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,n__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: add(X1,X2) -> n__add(X1,X2)
9: activate(n__fib1(X1,X2)) -> fib1(activate(X1),activate(X2))
10: activate(n__add(X1,X2)) -> add(activate(X1),activate(X2))
11: activate(X) -> X

There are 11 dependency pairs:

12: FIB(N) -> SEL(N,fib1(s(0),s(0)))
13: FIB(N) -> FIB1(s(0),s(0))
14: ADD(s(X),Y) -> ADD(X,Y)
15: SEL(s(N),cons(X,XS)) -> SEL(N,activate(XS))
16: SEL(s(N),cons(X,XS)) -> ACTIVATE(XS)
17: ACTIVATE(n__fib1(X1,X2)) -> FIB1(activate(X1),activate(X2))
18: ACTIVATE(n__fib1(X1,X2)) -> ACTIVATE(X1)
19: ACTIVATE(n__fib1(X1,X2)) -> ACTIVATE(X2)
20: ACTIVATE(n__add(X1,X2)) -> ADD(activate(X1),activate(X2))
21: ACTIVATE(n__add(X1,X2)) -> ACTIVATE(X1)
22: ACTIVATE(n__add(X1,X2)) -> ACTIVATE(X2)

The approximated dependency graph contains 3 SCCs:
{14},
{18,19,21,22}
and {15}.

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

- Consider the SCC {18,19,21,22}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = x + 1
and [n__add](x,y) = [n__fib1](x,y) = x + y + 1,
the rules in {18,19,21,22}
are strictly decreasing.

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

Hence the TRS is terminating.