Consider the TRS R consisting of the rewrite rules

1: D(t) -> 1
2: D(constant) -> 0
3: D(x + y) -> D(x) + D(y)
4: D(x * y) -> (y * D(x)) + (x * D(y))
5: D(x - y) -> D(x) - D(y)

There are 6 dependency pairs:

6: D#(x + y) -> D#(x)
7: D#(x + y) -> D#(y)
8: D#(x * y) -> D#(x)
9: D#(x * y) -> D#(y)
10: D#(x - y) -> D#(x)
11: D#(x - y) -> D#(y)

The approximated dependency graph contains one SCC:
{6-11}.

- Consider the SCC {6-11}.
There are no usable rules.
By taking the polynomial interpretation
[D#](x) = x + 1
and [*](x,y) = [+](x,y) = [-](x,y) = x + y + 1,
the rules in {6-11}
are strictly decreasing.

Hence the TRS is terminating.