YES

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

The following DP Processors were used


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

Problem 1: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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