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