YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (11ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

+#(*(x, y), *(a, y))+#(x, a)*#(*(x, y), z)*#(x, *(y, z))
*#(*(x, y), z)*#(y, z)+#(*(x, y), *(a, y))*#(+(x, a), y)

Rewrite Rules

+(*(x, y), *(a, y))*(+(x, a), y)*(*(x, y), z)*(x, *(y, z))

Original Signature

Termination of terms over the following signature is verified: a, *, +

Strategy


The following SCCs where found

*#(*(x, y), z) → *#(x, *(y, z))*#(*(x, y), z) → *#(y, z)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

*#(*(x, y), z)*#(x, *(y, z))*#(*(x, y), z)*#(y, z)

Rewrite Rules

+(*(x, y), *(a, y))*(+(x, a), y)*(*(x, y), z)*(x, *(y, z))

Original Signature

Termination of terms over the following signature is verified: a, *, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

*#(*(x, y), z)*#(y, z)*#(*(x, y), z)*#(x, *(y, z))