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))

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'(*(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)

Furthermore, R contains one SCC.


SCC1:

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)

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(D'(x_1)) = 1 + x_1
POL(+(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   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)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.597 seconds.