The TRS could be proven terminating. The proof took 122 ms.
Problem 1 was processed with processor SubtermCriterion (0ms). | – Problem 2 was processed with processor PolynomialLinearRange4iUR (94ms). | | – Problem 3 was processed with processor DependencyGraph (1ms).
| quot#(x, 0, s(z)) | → | div#(x, s(z)) | div#(x, y) | → | quot#(x, y, y) | |
| quot#(s(x), s(y), z) | → | quot#(x, y, z) |
| div(0, y) | → | 0 | div(x, y) | → | quot(x, y, y) | |
| quot(0, s(y), z) | → | 0 | quot(s(x), s(y), z) | → | quot(x, y, z) | |
| quot(x, 0, s(z)) | → | s(div(x, s(z))) |
Termination of terms over the following signature is verified: 0, s, div, quot
The following projection was used:
Thus, the following dependency pairs are removed:
| quot#(s(x), s(y), z) | → | quot#(x, y, z) |
| quot#(x, 0, s(z)) | → | div#(x, s(z)) | div#(x, y) | → | quot#(x, y, y) |
| div(0, y) | → | 0 | div(x, y) | → | quot(x, y, y) | |
| quot(0, s(y), z) | → | 0 | quot(s(x), s(y), z) | → | quot(x, y, z) | |
| quot(x, 0, s(z)) | → | s(div(x, s(z))) |
Termination of terms over the following signature is verified: 0, s, div, quot
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| div#(x, y) | → | quot#(x, y, y) |
| quot#(x, 0, s(z)) | → | div#(x, s(z)) |
| div(0, y) | → | 0 | div(x, y) | → | quot(x, y, y) | |
| quot(0, s(y), z) | → | 0 | quot(s(x), s(y), z) | → | quot(x, y, z) | |
| quot(x, 0, s(z)) | → | s(div(x, s(z))) |
Termination of terms over the following signature is verified: 0, s, div, quot