The TRS could be proven terminating. The proof took 17 ms.
Problem 1 was processed with processor SubtermCriterion (1ms). | – Problem 2 was processed with processor DependencyGraph (1ms).
| quot#(x, 0, s(z)) | → | quot#(x, s(z), s(z)) | quot#(s(x), s(y), z) | → | quot#(x, y, z) |
| quot(0, s(y), s(z)) | → | 0 | quot(s(x), s(y), z) | → | quot(x, y, z) | |
| quot(x, 0, s(z)) | → | s(quot(x, s(z), s(z))) |
Termination of terms over the following signature is verified: 0, s, 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)) | → | quot#(x, s(z), s(z)) |
| quot(0, s(y), s(z)) | → | 0 | quot(s(x), s(y), z) | → | quot(x, y, z) | |
| quot(x, 0, s(z)) | → | s(quot(x, s(z), s(z))) |
Termination of terms over the following signature is verified: 0, s, quot