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)
6: D(minus(x)) -> minus(D(x))
7: D(div(x,y)) -> div(D(x),y) - div(x * D(y),pow(y,2))
8: D(ln(x)) -> div(D(x),x)
9: D(pow(x,y)) -> ((y * pow(x,y - 1)) * D(x)) + ((pow(x,y) * ln(x)) * D(y))

There are 12 dependency pairs:

10: D#(x + y) -> D#(x)
11: D#(x + y) -> D#(y)
12: D#(x * y) -> D#(x)
13: D#(x * y) -> D#(y)
14: D#(x - y) -> D#(x)
15: D#(x - y) -> D#(y)
16: D#(minus(x)) -> D#(x)
17: D#(div(x,y)) -> D#(x)
18: D#(div(x,y)) -> D#(y)
19: D#(ln(x)) -> D#(x)
20: D#(pow(x,y)) -> D#(x)
21: D#(pow(x,y)) -> D#(y)

The approximated dependency graph contains one SCC:
{10-21}.

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

Hence the TRS is terminating.