The TRS could be proven terminating. The proof took 77 ms.
Problem 1 was processed with processor DependencyGraph (3ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (41ms).
| minus#(x, s(y)) | → | minus#(x, y) | minus#(x, s(y)) | → | U11#(minus(x, y), y, x) |
| minus(x, 0) | → | x | minus(x, s(y)) | → | U11(minus(x, y), y, x) | |
| U11(s(z), y, x) | → | z |
Termination of terms over the following signature is verified: minus, 0, s
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(s) = μ(U11) = {1}
μ(minus) = μ(minus#) = {1, 2}
| minus#(x, s(y)) → minus#(x, y) |
| minus#(x, s(y)) | → | minus#(x, y) |
| minus(x, 0) | → | x | minus(x, s(y)) | → | U11(minus(x, y), y, x) | |
| U11(s(z), y, x) | → | z |
Termination of terms over the following signature is verified: minus, 0, s
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(s) = μ(U11) = {1}
μ(minus) = μ(minus#) = {1, 2}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| minus#(x, s(y)) | → | minus#(x, y) |