Consider the TRS R consisting of the rewrite rules

1: half(0) -> 0
2: half(s(s(x))) -> s(half(x))
3: log(s(0)) -> 0
4: log(s(s(x))) -> s(log(s(half(x))))

There are 3 dependency pairs:

5: HALF(s(s(x))) -> HALF(x)
6: LOG(s(s(x))) -> LOG(s(half(x)))
7: LOG(s(s(x))) -> HALF(x)

The approximated dependency graph contains 2 SCCs:
{5}
and {6}.

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

- Consider the SCC {6}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = 1,
[half](x) = x
and [LOG](x) = [s](x) = x + 1,
rule 1
is weakly decreasing and
the rules in {2,6}
are strictly decreasing.

Hence the TRS is terminating.