The TRS could be proven terminating. The proof took 890 ms.
Problem 1 was processed with processor DependencyGraph (114ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (138ms). | | – Problem 3 was processed with processor PolynomialLinearRange4 (138ms). | | | – Problem 4 was processed with processor PolynomialLinearRange4 (152ms). | | | | – Problem 5 was processed with processor PolynomialLinearRange4 (53ms).
| T(zip(XS, YS)) | → | zip#(XS, YS) | T(zip(x_1, x_2)) | → | T(x_1) | |
| T(oddNs) | → | oddNs# | T(incr(oddNs)) | → | incr#(oddNs) | |
| T(repItems(XS)) | → | repItems#(XS) | T(cons(x_1, x_2)) | → | T(x_2) | |
| oddNs# | → | incr#(pairNs) | tail#(cons(X, XS)) | → | T(XS) | |
| T(take(x_1, x_2)) | → | T(x_1) | T(cons(x_1, x_2)) | → | T(x_1) | |
| T(incr(XS)) | → | incr#(XS) | T(zip(x_1, x_2)) | → | T(x_2) | |
| T(repItems(x_1)) | → | T(x_1) | T(take(x_1, x_2)) | → | T(x_2) | |
| T(take(N, XS)) | → | take#(N, XS) | T(incr(x_1)) | → | T(x_1) | |
| oddNs# | → | pairNs# |
| pairNs | → | cons(0, incr(oddNs)) | oddNs | → | incr(pairNs) | |
| incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | take(0, XS) | → | nil | |
| take(s(N), cons(X, XS)) | → | cons(X, take(N, XS)) | zip(nil, XS) | → | nil | |
| zip(X, nil) | → | nil | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), zip(XS, YS)) | |
| tail(cons(X, XS)) | → | XS | repItems(nil) | → | nil | |
| repItems(cons(X, XS)) | → | cons(X, cons(X, repItems(XS))) |
Termination of terms over the following signature is verified: zip, 0, pairNs, s, pair, take, repItems, incr, oddNs, tail, cons, nil
Context-sensitive strategy:
μ(oddNs#) = μ(T) = μ(pairNs#) = μ(0) = μ(pairNs) = μ(oddNs) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(repItems#) = μ(repItems) = μ(incr) = μ(cons) = {1}
μ(zip) = μ(pair) = μ(zip#) = μ(take#) = μ(take) = {1, 2}
| T(take(x_1, x_2)) → T(x_2) | T(zip(x_1, x_2)) → T(x_1) |
| T(incr(x_1)) → T(x_1) | T(cons(x_1, x_2)) → T(x_2) |
| T(take(x_1, x_2)) → T(x_1) | T(cons(x_1, x_2)) → T(x_1) |
| T(zip(x_1, x_2)) → T(x_2) | T(repItems(x_1)) → T(x_1) |
| T(take(x_1, x_2)) | → | T(x_2) | T(zip(x_1, x_2)) | → | T(x_1) | |
| T(incr(x_1)) | → | T(x_1) | T(cons(x_1, x_2)) | → | T(x_2) | |
| T(take(x_1, x_2)) | → | T(x_1) | T(cons(x_1, x_2)) | → | T(x_1) | |
| T(zip(x_1, x_2)) | → | T(x_2) | T(repItems(x_1)) | → | T(x_1) |
| pairNs | → | cons(0, incr(oddNs)) | oddNs | → | incr(pairNs) | |
| incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | take(0, XS) | → | nil | |
| take(s(N), cons(X, XS)) | → | cons(X, take(N, XS)) | zip(nil, XS) | → | nil | |
| zip(X, nil) | → | nil | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), zip(XS, YS)) | |
| tail(cons(X, XS)) | → | XS | repItems(nil) | → | nil | |
| repItems(cons(X, XS)) | → | cons(X, cons(X, repItems(XS))) |
Termination of terms over the following signature is verified: zip, 0, pairNs, s, pair, take, repItems, incr, oddNs, tail, cons, nil
Context-sensitive strategy:
μ(oddNs#) = μ(T) = μ(pairNs#) = μ(0) = μ(pairNs) = μ(oddNs) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(repItems) = μ(repItems#) = μ(incr) = μ(cons) = {1}
μ(zip) = μ(pair) = μ(zip#) = μ(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(cons(x_1, x_2)) | → | T(x_2) | T(cons(x_1, x_2)) | → | T(x_1) | |
| T(repItems(x_1)) | → | T(x_1) |
| T(zip(x_1, x_2)) | → | T(x_1) | T(take(x_1, x_2)) | → | T(x_2) | |
| T(incr(x_1)) | → | T(x_1) | T(take(x_1, x_2)) | → | T(x_1) | |
| T(zip(x_1, x_2)) | → | T(x_2) |
| pairNs | → | cons(0, incr(oddNs)) | oddNs | → | incr(pairNs) | |
| incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | take(0, XS) | → | nil | |
| take(s(N), cons(X, XS)) | → | cons(X, take(N, XS)) | zip(nil, XS) | → | nil | |
| zip(X, nil) | → | nil | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), zip(XS, YS)) | |
| tail(cons(X, XS)) | → | XS | repItems(nil) | → | nil | |
| repItems(cons(X, XS)) | → | cons(X, cons(X, repItems(XS))) |
Termination of terms over the following signature is verified: zip, 0, s, pairNs, pair, repItems, take, incr, tail, oddNs, nil, cons
Context-sensitive strategy:
μ(oddNs#) = μ(T) = μ(pairNs#) = μ(0) = μ(pairNs) = μ(oddNs) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(repItems#) = μ(repItems) = μ(incr) = μ(cons) = {1}
μ(zip) = μ(pair) = μ(zip#) = μ(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) |
| T(zip(x_1, x_2)) | → | T(x_1) | T(incr(x_1)) | → | T(x_1) | |
| T(zip(x_1, x_2)) | → | T(x_2) |
| pairNs | → | cons(0, incr(oddNs)) | oddNs | → | incr(pairNs) | |
| incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | take(0, XS) | → | nil | |
| take(s(N), cons(X, XS)) | → | cons(X, take(N, XS)) | zip(nil, XS) | → | nil | |
| zip(X, nil) | → | nil | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), zip(XS, YS)) | |
| tail(cons(X, XS)) | → | XS | repItems(nil) | → | nil | |
| repItems(cons(X, XS)) | → | cons(X, cons(X, repItems(XS))) |
Termination of terms over the following signature is verified: zip, 0, pairNs, s, pair, take, repItems, incr, oddNs, tail, cons, nil
Context-sensitive strategy:
μ(oddNs#) = μ(T) = μ(pairNs#) = μ(0) = μ(pairNs) = μ(oddNs) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(repItems) = μ(repItems#) = μ(incr) = μ(cons) = {1}
μ(zip) = μ(pair) = μ(zip#) = μ(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(incr(x_1)) | → | T(x_1) |
| T(zip(x_1, x_2)) | → | T(x_1) | T(zip(x_1, x_2)) | → | T(x_2) |
| pairNs | → | cons(0, incr(oddNs)) | oddNs | → | incr(pairNs) | |
| incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | take(0, XS) | → | nil | |
| take(s(N), cons(X, XS)) | → | cons(X, take(N, XS)) | zip(nil, XS) | → | nil | |
| zip(X, nil) | → | nil | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), zip(XS, YS)) | |
| tail(cons(X, XS)) | → | XS | repItems(nil) | → | nil | |
| repItems(cons(X, XS)) | → | cons(X, cons(X, repItems(XS))) |
Termination of terms over the following signature is verified: zip, 0, s, pairNs, pair, repItems, take, incr, tail, oddNs, nil, cons
Context-sensitive strategy:
μ(oddNs#) = μ(T) = μ(pairNs#) = μ(0) = μ(pairNs) = μ(oddNs) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(repItems#) = μ(repItems) = μ(incr) = μ(cons) = {1}
μ(zip) = μ(pair) = μ(zip#) = μ(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(zip(x_1, x_2)) | → | T(x_1) | T(zip(x_1, x_2)) | → | T(x_2) |