Term Rewriting System R:

   [x, y]
   D(t) -> 1
   D(constant) -> 0
   D(+(x, y)) -> +(D(x), D(y))
   D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
   D(-(x, y)) -> -(D(x), D(y))
   D(minus(x)) -> minus(D(x))
   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2)))
   D(ln(x)) -> div(D(x), x)
   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1))), D(x)), *(*(pow(x, y), ln(x)), D(y)))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   D'(ln(x)) -> D'(x)
   D'(*(x, y)) -> D'(x)
   D'(*(x, y)) -> D'(y)
   D'(-(x, y)) -> D'(x)
   D'(-(x, y)) -> D'(y)
   D'(+(x, y)) -> D'(x)
   D'(+(x, y)) -> D'(y)
   D'(div(x, y)) -> D'(x)
   D'(div(x, y)) -> D'(y)
   D'(pow(x, y)) -> D'(x)
   D'(pow(x, y)) -> D'(y)
   D'(minus(x)) -> D'(x)

Furthermore, R contains one SCC.


SCC1:

D'(minus(x)) -> D'(x)
D'(pow(x, y)) -> D'(y)
D'(pow(x, y)) -> D'(x)
D'(div(x, y)) -> D'(y)
D'(div(x, y)) -> D'(x)
D'(+(x, y)) -> D'(y)
D'(+(x, y)) -> D'(x)
D'(-(x, y)) -> D'(y)
D'(-(x, y)) -> D'(x)
D'(*(x, y)) -> D'(y)
D'(*(x, y)) -> D'(x)
D'(ln(x)) -> D'(x)

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(*(x_1, x_2)) = 1 + x_1 + x_2
POL(-(x_1, x_2)) = 1 + x_1 + x_2
POL(minus(x_1)) = 1 + x_1
POL(div(x_1, x_2)) = 1 + x_1 + x_2
POL(ln(x_1)) = 1 + x_1
POL(D'(x_1)) = 1 + x_1
POL(+(x_1, x_2)) = 1 + x_1 + x_2
POL(pow(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   D'(minus(x)) -> D'(x)
   D'(pow(x, y)) -> D'(y)
   D'(pow(x, y)) -> D'(x)
   D'(div(x, y)) -> D'(y)
   D'(div(x, y)) -> D'(x)
   D'(+(x, y)) -> D'(y)
   D'(+(x, y)) -> D'(x)
   D'(-(x, y)) -> D'(y)
   D'(-(x, y)) -> D'(x)
   D'(*(x, y)) -> D'(y)
   D'(*(x, y)) -> D'(x)
   D'(ln(x)) -> D'(x)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 1.106 seconds.