The TRS could be proven terminating. The proof took 307 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (168ms). | – Problem 2 was processed with processor PolynomialLinearRange4iUR (40ms).
average#(x, s(s(s(y)))) | → | average#(s(x), y) | average#(s(x), y) | → | average#(x, s(y)) |
average(s(x), y) | → | average(x, s(y)) | average(x, s(s(s(y)))) | → | s(average(s(x), y)) | |
average(0, 0) | → | 0 | average(0, s(0)) | → | 0 | |
average(0, s(s(0))) | → | s(0) |
Termination of terms over the following signature is verified: 0, s, average
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
average#(x, s(s(s(y)))) | → | average#(s(x), y) |
average#(s(x), y) | → | average#(x, s(y)) |
average(s(x), y) | → | average(x, s(y)) | average(x, s(s(s(y)))) | → | s(average(s(x), y)) | |
average(0, 0) | → | 0 | average(0, s(0)) | → | 0 | |
average(0, s(s(0))) | → | s(0) |
Termination of terms over the following signature is verified: 0, s, average
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
average#(s(x), y) | → | average#(x, s(y)) |