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