The TRS could be proven terminating. The proof took 120 ms.
Problem 1 was processed with processor DependencyGraph (6ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (69ms). | | – Problem 3 was processed with processor PolynomialLinearRange4 (16ms).
| T(s(x_1)) | → | T(x_1) | T(from(x_1)) | → | T(x_1) | |
| 2nd#(cons(X, cons(Y, Z))) | → | T(Y) | T(from(s(X))) | → | from#(s(X)) |
| 2nd(cons(X, cons(Y, Z))) | → | Y | from(X) | → | cons(X, from(s(X))) |
Termination of terms over the following signature is verified: 2nd, s, from, cons
Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(from#) = μ(s) = μ(2nd#) = μ(from) = μ(cons) = {1}
| T(s(x_1)) → T(x_1) | T(from(x_1)) → T(x_1) |
| T(s(x_1)) | → | T(x_1) | T(from(x_1)) | → | T(x_1) |
| 2nd(cons(X, cons(Y, Z))) | → | Y | from(X) | → | cons(X, from(s(X))) |
Termination of terms over the following signature is verified: 2nd, s, from, cons
Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(s) = μ(from#) = μ(from) = μ(2nd#) = μ(cons) = {1}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(s(x_1)) | → | T(x_1) |
| T(from(x_1)) | → | T(x_1) |
| 2nd(cons(X, cons(Y, Z))) | → | Y | from(X) | → | cons(X, from(s(X))) |
Termination of terms over the following signature is verified: 2nd, s, from, cons
Context-sensitive strategy:
μ(T) = ∅
μ(2nd) = μ(from#) = μ(s) = μ(2nd#) = μ(from) = μ(cons) = {1}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(from(x_1)) | → | T(x_1) |