Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

9: F(X) -> IF(X,c,n__f(n__true))
10: IF(false,X,Y) -> ACTIVATE(Y)
11: ACTIVATE(n__f(X)) -> F(activate(X))
12: ACTIVATE(n__f(X)) -> ACTIVATE(X)
13: ACTIVATE(n__true) -> TRUE

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

- Consider the SCC {9-12}.
By taking the polynomial interpretation
[c] = [n__true] = 0,
[false] = [true] = 1,
[activate](x) = [ACTIVATE](x) = [f](x) = [F](x) = [n__f](x) = x + 1
and [if](x,y,z) = [IF](x,y,z) = x + y + z,
the rules in {1,3,4,6,7,9-11}
are weakly decreasing and
the rules in {2,5,8,12}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {9-11}.
By taking the polynomial interpretation
[c] = [n__true] = [true] = 0,
[false] = 1,
[activate](x) = x,
[ACTIVATE](x) = [f](x) = [F](x) = [n__f](x) = x + 1
and [if](x,y,z) = [IF](x,y,z) = x + y + z,
the rules in {1,2,4-10}
are weakly decreasing and
the rules in {3,11}
are strictly decreasing.


Hence the TRS is terminating.