The TRS could be proven terminating. The proof took 155 ms.
Problem 1 was processed with processor DependencyGraph (14ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (63ms). | | – Problem 3 was processed with processor PolynomialLinearRange4 (40ms).
| from_3#(x) | → | cons_1#(x, from_3(s_0(x))) | from_1#(x) | → | T(x) | |
| from_2#(x) | → | from_3#(s_0(x)) | T(from_3(s_0(x))) | → | from_3#(s_0(x)) | |
| from_2#(x) | → | T(x) | from_1#(x) | → | from_3#(s_0(x)) | |
| T(s_0(x_1)) | → | T(x_1) | T(from_3(x_1)) | → | T(x_1) |
| from_2(x) | → | cons_0(x, from_3(s_0(x))) | from_3(x) | → | cons_1(x, from_3(s_0(x))) | |
| from_1(x) | → | cons_0(x, from_3(s_0(x))) | cons_1(s_0(x), xs) | → | overflow_0 |
Termination of terms over the following signature is verified: cons_1, overflow_0, cons_0, from_2, from_1, s_0, from_3
Context-sensitive strategy:
μ(from_2#) = μ(T) = μ(from_1#) = μ(cons_1#) = μ(cons_1) = μ(overflow_0) = μ(from_2) = μ(from_1) = μ(from_3#) = μ(from_3) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}
| T(s_0(x_1)) → T(x_1) | T(from_3(x_1)) → T(x_1) |
| T(s_0(x_1)) | → | T(x_1) | T(from_3(x_1)) | → | T(x_1) |
| from_2(x) | → | cons_0(x, from_3(s_0(x))) | from_3(x) | → | cons_1(x, from_3(s_0(x))) | |
| from_1(x) | → | cons_0(x, from_3(s_0(x))) | cons_1(s_0(x), xs) | → | overflow_0 |
Termination of terms over the following signature is verified: cons_1, overflow_0, cons_0, from_2, from_1, s_0, from_3
Context-sensitive strategy:
μ(T) = μ(from_2#) = μ(from_1#) = μ(cons_1#) = μ(overflow_0) = μ(cons_1) = μ(from_2) = μ(from_1) = μ(from_3) = μ(from_3#) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}
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_3(x_1)) | → | T(x_1) |
| T(s_0(x_1)) | → | T(x_1) |
| from_2(x) | → | cons_0(x, from_3(s_0(x))) | from_3(x) | → | cons_1(x, from_3(s_0(x))) | |
| from_1(x) | → | cons_0(x, from_3(s_0(x))) | cons_1(s_0(x), xs) | → | overflow_0 |
Termination of terms over the following signature is verified: overflow_0, cons_1, cons_0, from_2, from_1, s_0, from_3
Context-sensitive strategy:
μ(from_2#) = μ(T) = μ(from_1#) = μ(cons_1#) = μ(cons_1) = μ(overflow_0) = μ(from_2) = μ(from_1) = μ(from_3#) = μ(from_3) = ∅
μ(s_0) = {1}
μ(cons_0) = {1, 2}
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_0(x_1)) | → | T(x_1) |