Consider the TRS R consisting of the rewrite rules

1: dx(X) -> one
2: dx(a) -> zero
3: dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
4: dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
5: dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
6: dx(neg(ALPHA)) -> neg(dx(ALPHA))
7: dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))
8: dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
9: dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))

There are 12 dependency pairs:

10: DX(plus(ALPHA,BETA)) -> DX(ALPHA)
11: DX(plus(ALPHA,BETA)) -> DX(BETA)
12: DX(times(ALPHA,BETA)) -> DX(ALPHA)
13: DX(times(ALPHA,BETA)) -> DX(BETA)
14: DX(minus(ALPHA,BETA)) -> DX(ALPHA)
15: DX(minus(ALPHA,BETA)) -> DX(BETA)
16: DX(neg(ALPHA)) -> DX(ALPHA)
17: DX(div(ALPHA,BETA)) -> DX(ALPHA)
18: DX(div(ALPHA,BETA)) -> DX(BETA)
19: DX(ln(ALPHA)) -> DX(ALPHA)
20: DX(exp(ALPHA,BETA)) -> DX(ALPHA)
21: DX(exp(ALPHA,BETA)) -> DX(BETA)

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

- Consider the SCC {10-21}.
There are no usable rules.
By taking the polynomial interpretation
[DX](x) = [ln](x) = [neg](x) = x + 1
and [div](x,y) = [exp](x,y) = [minus](x,y) = [plus](x,y) = [times](x,y) = x + y + 1,
the rules in {10-21}
are strictly decreasing.

Hence the TRS is terminating.