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