The TRS could be proven terminating. The proof took 21 ms.
Problem 1 was processed with processor SubtermCriterion (1ms).
| minus#(h(x)) | → | minus#(x) | minus#(f(x, y)) | → | minus#(x) | |
| minus#(f(x, y)) | → | minus#(y) |
| minus(minus(x)) | → | x | minus(h(x)) | → | h(minus(x)) | |
| minus(f(x, y)) | → | f(minus(y), minus(x)) |
Termination of terms over the following signature is verified: f, minus, h
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(h(x)) | → | minus#(x) | minus#(f(x, y)) | → | minus#(x) | |
| minus#(f(x, y)) | → | minus#(y) |