Consider the TRS R consisting of the rewrite rules

1: minus(minus(x)) -> x
2: minus(x + y) -> minus(minus(minus(x))) * minus(minus(minus(y)))
3: minus(x * y) -> minus(minus(minus(x))) + minus(minus(minus(y)))
4: f(minus(x)) -> minus(minus(minus(f(x))))

There are 16 dependency pairs:

5: MINUS(x + y) -> MINUS(minus(minus(x)))
6: MINUS(x + y) -> MINUS(minus(x))
7: MINUS(x + y) -> MINUS(x)
8: MINUS(x + y) -> MINUS(minus(minus(y)))
9: MINUS(x + y) -> MINUS(minus(y))
10: MINUS(x + y) -> MINUS(y)
11: MINUS(x * y) -> MINUS(minus(minus(x)))
12: MINUS(x * y) -> MINUS(minus(x))
13: MINUS(x * y) -> MINUS(x)
14: MINUS(x * y) -> MINUS(minus(minus(y)))
15: MINUS(x * y) -> MINUS(minus(y))
16: MINUS(x * y) -> MINUS(y)
17: F(minus(x)) -> MINUS(minus(minus(f(x))))
18: F(minus(x)) -> MINUS(minus(f(x)))
19: F(minus(x)) -> MINUS(f(x))
20: F(minus(x)) -> F(x)

The approximated dependency graph contains 2 SCCs:
{5-16}
and {20}.

- Consider the SCC {5-16}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[minus](x) = x,
[MINUS](x) = x + 1
and [*](x,y) = [+](x,y) = x + y + 1,
the rules in {1-3}
are weakly decreasing and
the rules in {5-16}
are strictly decreasing.

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

Hence the TRS is terminating.