The TRS could be proven terminating. The proof took 726 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (480ms). | – Problem 2 was processed with processor PolynomialLinearRange4iUR (78ms).
| f#(x, y) | → | ack#(x, y) | f#(x, s(y)) | → | f#(y, x) | |
| ack#(s(x), y) | → | f#(x, x) | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) | |
| ack#(s(x), s(y)) | → | ack#(s(x), y) | ack#(s(x), 0) | → | ack#(x, s(0)) | |
| f#(s(x), y) | → | f#(x, s(x)) |
| ack(0, y) | → | s(y) | ack(s(x), 0) | → | ack(x, s(0)) | |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) | f(s(x), y) | → | f(x, s(x)) | |
| f(x, s(y)) | → | f(y, x) | f(x, y) | → | ack(x, y) | |
| ack(s(x), y) | → | f(x, x) |
Termination of terms over the following signature is verified: f, 0, s, ack
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(x, y) | → | ack#(x, y) | ack#(s(x), y) | → | f#(x, x) | |
| f#(x, s(y)) | → | f#(y, x) | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) | |
| ack#(s(x), 0) | → | ack#(x, s(0)) | f#(s(x), y) | → | f#(x, s(x)) |
| ack#(s(x), s(y)) | → | ack#(s(x), y) |
| ack(0, y) | → | s(y) | ack(s(x), 0) | → | ack(x, s(0)) | |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) | f(s(x), y) | → | f(x, s(x)) | |
| f(x, s(y)) | → | f(y, x) | f(x, y) | → | ack(x, y) | |
| ack(s(x), y) | → | f(x, x) |
Termination of terms over the following signature is verified: f, 0, s, ack
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ack#(s(x), s(y)) | → | ack#(s(x), y) |