MAYBE
The TRS could not be proven terminating. The proof attempt took 2394 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor SubtermCriterion (0ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (12ms), PolynomialLinearRange4iUR (351ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (847ms), DependencyGraph (7ms), ReductionPairSAT (903ms), DependencyGraph (10ms), SizeChangePrinciple (55ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| *#(x, +(y, z)) | → | *#(x, z) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(+(y, z), x) | → | *#(x, z) | | *#(*(x, y), z) | → | *#(x, *(y, z)) |
| *#(*(x, y), z) | → | *#(y, z) | | *#(x, +(y, z)) | → | *#(x, y) |
Rewrite Rules
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| *(*(x, y), z) | → | *(x, *(y, z)) | | +(+(x, y), z) | → | +(x, +(y, z)) |
Original Signature
Termination of terms over the following signature is verified: *, +
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| *#(x, +(y, z)) | → | *#(x, z) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(x, +(y, z)) | → | +#(*(x, y), *(x, z)) | | *#(+(y, z), x) | → | *#(x, z) |
| *#(*(x, y), z) | → | *#(x, *(y, z)) | | *#(*(x, y), z) | → | *#(y, z) |
| +#(+(x, y), z) | → | +#(y, z) | | *#(x, +(y, z)) | → | *#(x, y) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |
Rewrite Rules
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| *(*(x, y), z) | → | *(x, *(y, z)) | | +(+(x, y), z) | → | +(x, +(y, z)) |
Original Signature
Termination of terms over the following signature is verified: *, +
Strategy
The following SCCs where found
| *#(x, +(y, z)) → *#(x, z) | *#(+(y, z), x) → *#(x, y) |
| *#(+(y, z), x) → *#(x, z) | *#(*(x, y), z) → *#(y, z) |
| *#(*(x, y), z) → *#(x, *(y, z)) | *#(x, +(y, z)) → *#(x, y) |
| +#(+(x, y), z) → +#(y, z) | +#(+(x, y), z) → +#(x, +(y, z)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| +#(+(x, y), z) | → | +#(y, z) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |
Rewrite Rules
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| *(*(x, y), z) | → | *(x, *(y, z)) | | +(+(x, y), z) | → | +(x, +(y, z)) |
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), z) | → | +#(y, z) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |