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