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