YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


The following SCCs where found

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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