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