Term Rewriting System R:

   [X, ALPHA, BETA]
   dx(X) -> one
   dx(a) -> zero
   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
   dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
   dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
   dx(neg(ALPHA)) -> neg(dx(ALPHA))
   dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
   dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
   dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   DX(times(ALPHA, BETA)) -> DX(ALPHA)
   DX(times(ALPHA, BETA)) -> DX(BETA)
   DX(ln(ALPHA)) -> DX(ALPHA)
   DX(exp(ALPHA, BETA)) -> DX(ALPHA)
   DX(exp(ALPHA, BETA)) -> DX(BETA)
   DX(neg(ALPHA)) -> DX(ALPHA)
   DX(minus(ALPHA, BETA)) -> DX(ALPHA)
   DX(minus(ALPHA, BETA)) -> DX(BETA)
   DX(div(ALPHA, BETA)) -> DX(ALPHA)
   DX(div(ALPHA, BETA)) -> DX(BETA)
   DX(plus(ALPHA, BETA)) -> DX(ALPHA)
   DX(plus(ALPHA, BETA)) -> DX(BETA)

Furthermore, R contains one SCC.


SCC1:

DX(plus(ALPHA, BETA)) -> DX(BETA)
DX(plus(ALPHA, BETA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(minus(ALPHA, BETA)) -> DX(BETA)
DX(minus(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(exp(ALPHA, BETA)) -> DX(BETA)
DX(exp(ALPHA, BETA)) -> DX(ALPHA)
DX(ln(ALPHA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(times(ALPHA, BETA)) -> DX(ALPHA)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(exp(x_1, x_2)) = 1 + x_1 + x_2
POL(plus(x_1, x_2)) = 1 + x_1 + x_2
POL(DX(x_1)) = 1 + x_1
POL(div(x_1, x_2)) = 1 + x_1 + x_2
POL(minus(x_1, x_2)) = 1 + x_1 + x_2
POL(ln(x_1)) = 1 + x_1
POL(neg(x_1)) = 1 + x_1
POL(times(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   DX(plus(ALPHA, BETA)) -> DX(BETA)
   DX(plus(ALPHA, BETA)) -> DX(ALPHA)
   DX(div(ALPHA, BETA)) -> DX(BETA)
   DX(div(ALPHA, BETA)) -> DX(ALPHA)
   DX(minus(ALPHA, BETA)) -> DX(BETA)
   DX(minus(ALPHA, BETA)) -> DX(ALPHA)
   DX(neg(ALPHA)) -> DX(ALPHA)
   DX(exp(ALPHA, BETA)) -> DX(BETA)
   DX(exp(ALPHA, BETA)) -> DX(ALPHA)
   DX(ln(ALPHA)) -> DX(ALPHA)
   DX(times(ALPHA, BETA)) -> DX(BETA)
   DX(times(ALPHA, BETA)) -> DX(ALPHA)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.954 seconds.