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