YES

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

The following DP Processors were used

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

Problem 1: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

dx^#(plus(ALPHA, BETA))	→	dx^#(BETA)		dx^#(exp(ALPHA, BETA))	→	dx^#(ALPHA)
dx^#(minus(ALPHA, BETA))	→	dx^#(BETA)		dx^#(exp(ALPHA, BETA))	→	dx^#(BETA)
dx^#(plus(ALPHA, BETA))	→	dx^#(ALPHA)		dx^#(times(ALPHA, BETA))	→	dx^#(BETA)
dx^#(minus(ALPHA, BETA))	→	dx^#(ALPHA)		dx^#(times(ALPHA, BETA))	→	dx^#(ALPHA)
dx^#(div(ALPHA, BETA))	→	dx^#(ALPHA)		dx^#(ln(ALPHA))	→	dx^#(ALPHA)
dx^#(neg(ALPHA))	→	dx^#(ALPHA)		dx^#(div(ALPHA, BETA))	→	dx^#(BETA)

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: plus, neg, two, exp, ln, minus, dx, times, one, a, div, zero

Strategy

Projection

The following projection was used:

π (dx#): 1

Thus, the following dependency pairs are removed:

dx^#(exp(ALPHA, BETA))	→	dx^#(ALPHA)		dx^#(plus(ALPHA, BETA))	→	dx^#(BETA)
dx^#(exp(ALPHA, BETA))	→	dx^#(BETA)		dx^#(minus(ALPHA, BETA))	→	dx^#(BETA)
dx^#(times(ALPHA, BETA))	→	dx^#(BETA)		dx^#(plus(ALPHA, BETA))	→	dx^#(ALPHA)
dx^#(minus(ALPHA, BETA))	→	dx^#(ALPHA)		dx^#(times(ALPHA, BETA))	→	dx^#(ALPHA)
dx^#(ln(ALPHA))	→	dx^#(ALPHA)		dx^#(div(ALPHA, BETA))	→	dx^#(ALPHA)
dx^#(neg(ALPHA))	→	dx^#(ALPHA)		dx^#(div(ALPHA, BETA))	→	dx^#(BETA)