Consider the TRS R consisting of the rewrite rules

1: f(X) -> if(X,c,n__f(true))
2: if(true,X,Y) -> X
3: if(false,X,Y) -> activate(Y)
4: f(X) -> n__f(X)
5: activate(n__f(X)) -> f(X)
6: activate(X) -> X

There are 3 dependency pairs:

7: F(X) -> IF(X,c,n__f(true))
8: IF(false,X,Y) -> ACTIVATE(Y)
9: ACTIVATE(n__f(X)) -> F(X)

The approximated dependency graph contains one SCC:
{7-9}.

- Consider the SCC {7-9}.
There are no usable rules.
By taking the polynomial interpretation
[true] = 0,
[c] = [false] = 1,
[ACTIVATE](x) = [F](x) = [n__f](x) = x + 1
and [IF](x,y,z) = x + z,
the rules in {7,8}
are weakly decreasing and
rule 9
is strictly decreasing.

Hence the TRS is terminating.