The TRS could be proven terminating. The proof took 311 ms.
Problem 1 was processed with processor SubtermCriterion (20ms).
| D#(*(x, y)) | → | D#(y) | D#(+(x, y)) | → | D#(y) | |
| D#(*(x, y)) | → | D#(x) | D#(ln(x)) | → | D#(x) | |
| D#(minus(x)) | → | D#(x) | D#(pow(x, y)) | → | D#(x) | |
| D#(div(x, y)) | → | D#(x) | D#(div(x, y)) | → | D#(y) | |
| D#(-(x, y)) | → | D#(x) | D#(pow(x, y)) | → | D#(y) | |
| D#(+(x, y)) | → | D#(x) | D#(-(x, y)) | → | D#(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 terms over the following signature is verified: D, ln, constant, minus, pow, *, div, +, -, 2, 1, t, 0
The following projection was used:
Thus, the following dependency pairs are removed:
| D#(*(x, y)) | → | D#(y) | D#(+(x, y)) | → | D#(y) | |
| D#(ln(x)) | → | D#(x) | D#(*(x, y)) | → | D#(x) | |
| D#(minus(x)) | → | D#(x) | D#(pow(x, y)) | → | D#(x) | |
| D#(div(x, y)) | → | D#(y) | D#(div(x, y)) | → | D#(x) | |
| D#(-(x, y)) | → | D#(x) | D#(pow(x, y)) | → | D#(y) | |
| D#(+(x, y)) | → | D#(x) | D#(-(x, y)) | → | D#(y) |