YES

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

The following DP Processors were used

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

Problem 1: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

D^#(*(x, y))	→	D^#(y)		D^#(+(x, y))	→	D^#(y)
D^#(*(x, y))	→	D^#(x)		D^#(-(x, y))	→	D^#(x)
D^#(+(x, y))	→	D^#(x)		D^#(-(x, y))	→	D^#(y)

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: D, 1, t, 0, constant, *, +, -

Strategy

Projection

The following projection was used:

π (D#): 1

Thus, the following dependency pairs are removed:

D^#(*(x, y))	→	D^#(y)		D^#(+(x, y))	→	D^#(y)
D^#(*(x, y))	→	D^#(x)		D^#(-(x, y))	→	D^#(x)
D^#(+(x, y))	→	D^#(x)		D^#(-(x, y))	→	D^#(y)