YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

+#(x, minus(y))+#(minus(x), y)+#(x, minus(y))minus#(+(minus(x), y))
+#(x, +(y, z))+#(+(x, y), z)+#(minus(+(x, 1)), 1)minus#(x)
+#(x, minus(y))minus#(x)+#(x, +(y, z))+#(x, y)

Rewrite Rules

minus(0)0+(x, 0)x
+(0, y)y+(minus(1), 1)0
minus(minus(x))x+(x, minus(y))minus(+(minus(x), y))
+(x, +(y, z))+(+(x, y), z)+(minus(+(x, 1)), 1)minus(x)

Original Signature

Termination of terms over the following signature is verified: 1, minus, 0, +

Strategy


The following SCCs where found

+#(x, minus(y)) → +#(minus(x), y)+#(x, +(y, z)) → +#(+(x, y), z)
+#(x, +(y, z)) → +#(x, y)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

+#(x, minus(y))+#(minus(x), y)+#(x, +(y, z))+#(+(x, y), z)
+#(x, +(y, z))+#(x, y)

Rewrite Rules

minus(0)0+(x, 0)x
+(0, y)y+(minus(1), 1)0
minus(minus(x))x+(x, minus(y))minus(+(minus(x), y))
+(x, +(y, z))+(+(x, y), z)+(minus(+(x, 1)), 1)minus(x)

Original Signature

Termination of terms over the following signature is verified: 1, minus, 0, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

+#(x, minus(y))+#(minus(x), y)+#(x, +(y, z))+#(+(x, y), z)
+#(x, +(y, z))+#(x, y)