YES

The TRS could be proven terminating. The proof took 311 ms.

The following DP Processors were used


Problem 1 was processed with processor SubtermCriterion (20ms).

Problem 1: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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)

Rewrite Rules

D(t)1D(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)))

Original Signature

Termination of terms over the following signature is verified: D, ln, constant, minus, pow, *, div, +, -, 2, 1, t, 0

Strategy


Projection

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)