YES
The TRS could be proven terminating. The proof took 50 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (27ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| minus#(+(x, y)) | → | +#(minus(y), minus(x)) | | *#(x, +(y, z)) | → | *#(x, z) |
| *#(x, minus(y)) | → | minus#(*(x, y)) | | *#(x, minus(y)) | → | *#(x, y) |
| minus#(+(x, y)) | → | minus#(x) | | *#(x, +(y, z)) | → | +#(*(x, y), *(x, z)) |
| minus#(+(x, y)) | → | minus#(y) | | *#(x, +(y, z)) | → | *#(x, y) |
Rewrite Rules
| +(x, 0) | → | x | | +(minus(x), x) | → | 0 |
| minus(0) | → | 0 | | minus(minus(x)) | → | x |
| minus(+(x, y)) | → | +(minus(y), minus(x)) | | *(x, 1) | → | x |
| *(x, 0) | → | 0 | | *(x, +(y, z)) | → | +(*(x, y), *(x, z)) |
| *(x, minus(y)) | → | minus(*(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, minus, *, +
Strategy
The following SCCs where found
| minus#(+(x, y)) → minus#(x) | minus#(+(x, y)) → minus#(y) |
| *#(x, +(y, z)) → *#(x, z) | *#(x, minus(y)) → *#(x, y) |
| *#(x, +(y, z)) → *#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(+(x, y)) | → | minus#(x) | | minus#(+(x, y)) | → | minus#(y) |
Rewrite Rules
| +(x, 0) | → | x | | +(minus(x), x) | → | 0 |
| minus(0) | → | 0 | | minus(minus(x)) | → | x |
| minus(+(x, y)) | → | +(minus(y), minus(x)) | | *(x, 1) | → | x |
| *(x, 0) | → | 0 | | *(x, +(y, z)) | → | +(*(x, y), *(x, z)) |
| *(x, minus(y)) | → | minus(*(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, minus, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(+(x, y)) | → | minus#(x) | | minus#(+(x, y)) | → | minus#(y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| *#(x, +(y, z)) | → | *#(x, z) | | *#(x, minus(y)) | → | *#(x, y) |
| *#(x, +(y, z)) | → | *#(x, y) |
Rewrite Rules
| +(x, 0) | → | x | | +(minus(x), x) | → | 0 |
| minus(0) | → | 0 | | minus(minus(x)) | → | x |
| minus(+(x, y)) | → | +(minus(y), minus(x)) | | *(x, 1) | → | x |
| *(x, 0) | → | 0 | | *(x, +(y, z)) | → | +(*(x, y), *(x, z)) |
| *(x, minus(y)) | → | minus(*(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, minus, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| *#(x, +(y, z)) | → | *#(x, z) | | *#(x, minus(y)) | → | *#(x, y) |
| *#(x, +(y, z)) | → | *#(x, y) |