The TRS could be proven terminating. The proof took 616 ms.
Problem 1 was processed with processor DependencyGraph (38ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (89ms). | – Problem 3 was processed with processor PolynomialLinearRange4 (44ms). | | – Problem 4 was processed with processor PolynomialLinearRange4 (123ms). | | | – Problem 5 was processed with processor PolynomialLinearRange4 (69ms).
| T(take(X, L)) | → | take#(X, L) | T(length(L)) | → | length#(L) | |
| T(take(x_1, x_2)) | → | T(x_2) | T(s(x_1)) | → | T(x_1) | |
| T(take(x_1, x_2)) | → | T(x_1) | T(length(x_1)) | → | T(x_1) | |
| eq#(s(X), s(Y)) | → | eq#(X, Y) | T(inf(s(X))) | → | inf#(s(X)) |
| eq(0, 0) | → | true | eq(s(X), s(Y)) | → | eq(X, Y) | |
| eq(X, Y) | → | false | inf(X) | → | cons(X, inf(s(X))) | |
| take(0, X) | → | nil | take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) | |
| length(nil) | → | 0 | length(cons(X, L)) | → | s(length(L)) |
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, false, eq, cons, nil
Context-sensitive strategy:
μ(true) = μ(eq#) = μ(T) = μ(0) = μ(s) = μ(false) = μ(eq) = μ(cons) = μ(nil) = ∅
μ(length#) = μ(inf) = μ(inf#) = μ(length) = {1}
μ(take#) = μ(take) = {1, 2}
| T(take(x_1, x_2)) → T(x_2) | T(s(x_1)) → T(x_1) |
| T(take(x_1, x_2)) → T(x_1) | T(length(x_1)) → T(x_1) |
| eq#(s(X), s(Y)) → eq#(X, Y) |
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
| eq(0, 0) | → | true | eq(s(X), s(Y)) | → | eq(X, Y) | |
| eq(X, Y) | → | false | inf(X) | → | cons(X, inf(s(X))) | |
| take(0, X) | → | nil | take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) | |
| length(nil) | → | 0 | length(cons(X, L)) | → | s(length(L)) |
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, false, eq, cons, nil
Context-sensitive strategy:
μ(true) = μ(eq#) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = μ(eq) = ∅
μ(length#) = μ(inf) = μ(inf#) = μ(length) = {1}
μ(take#) = μ(take) = {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:
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
| T(take(x_1, x_2)) | → | T(x_2) | T(s(x_1)) | → | T(x_1) | |
| T(take(x_1, x_2)) | → | T(x_1) | T(length(x_1)) | → | T(x_1) |
| eq(0, 0) | → | true | eq(s(X), s(Y)) | → | eq(X, Y) | |
| eq(X, Y) | → | false | inf(X) | → | cons(X, inf(s(X))) | |
| take(0, X) | → | nil | take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) | |
| length(nil) | → | 0 | length(cons(X, L)) | → | s(length(L)) |
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, false, eq, cons, nil
Context-sensitive strategy:
μ(true) = μ(eq#) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = μ(eq) = ∅
μ(length#) = μ(inf) = μ(inf#) = μ(length) = {1}
μ(take#) = μ(take) = {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(x_1)) | → | T(x_1) |
| T(take(x_1, x_2)) | → | T(x_2) | T(take(x_1, x_2)) | → | T(x_1) | |
| T(length(x_1)) | → | T(x_1) |
| eq(0, 0) | → | true | eq(s(X), s(Y)) | → | eq(X, Y) | |
| eq(X, Y) | → | false | inf(X) | → | cons(X, inf(s(X))) | |
| take(0, X) | → | nil | take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) | |
| length(nil) | → | 0 | length(cons(X, L)) | → | s(length(L)) |
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, true, nil, cons, eq
Context-sensitive strategy:
μ(true) = μ(eq#) = μ(T) = μ(0) = μ(s) = μ(false) = μ(eq) = μ(cons) = μ(nil) = ∅
μ(length#) = μ(inf) = μ(inf#) = μ(length) = {1}
μ(take#) = μ(take) = {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(length(x_1)) | → | T(x_1) |
| T(take(x_1, x_2)) | → | T(x_2) | T(take(x_1, x_2)) | → | T(x_1) |
| eq(0, 0) | → | true | eq(s(X), s(Y)) | → | eq(X, Y) | |
| eq(X, Y) | → | false | inf(X) | → | cons(X, inf(s(X))) | |
| take(0, X) | → | nil | take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) | |
| length(nil) | → | 0 | length(cons(X, L)) | → | s(length(L)) |
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, false, eq, cons, nil
Context-sensitive strategy:
μ(true) = μ(eq#) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = μ(eq) = ∅
μ(length#) = μ(inf) = μ(inf#) = μ(length) = {1}
μ(take#) = μ(take) = {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(take(x_1, x_2)) | → | T(x_2) | T(take(x_1, x_2)) | → | T(x_1) |