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