The TRS could be proven terminating. The proof took 101 ms.
Problem 1 was processed with processor DependencyGraph (18ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (51ms).
| T(incr(nats)) | → | incr#(nats) | T(nats) | → | nats# | |
| odds# | → | pairs# | T(incr(x_1)) | → | T(x_1) | |
| tail#(cons(X, XS)) | → | T(XS) | T(incr(odds)) | → | incr#(odds) | |
| T(incr(XS)) | → | incr#(XS) | odds# | → | incr#(pairs) | |
| T(odds) | → | odds# |
| nats | → | cons(0, incr(nats)) | pairs | → | cons(0, incr(odds)) | |
| odds | → | incr(pairs) | incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | |
| head(cons(X, XS)) | → | X | tail(cons(X, XS)) | → | XS |
Termination of terms over the following signature is verified: nats, 0, pairs, s, incr, head, odds, tail, cons
Context-sensitive strategy:
μ(pairs) = μ(odds#) = μ(odds) = μ(T) = μ(nats) = μ(0) = μ(nats#) = μ(nil) = μ(pairs#) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(head#) = μ(incr) = μ(head) = μ(cons) = {1}
| T(incr(x_1)) → T(x_1) |
| T(incr(x_1)) | → | T(x_1) |
| nats | → | cons(0, incr(nats)) | pairs | → | cons(0, incr(odds)) | |
| odds | → | incr(pairs) | incr(cons(X, XS)) | → | cons(s(X), incr(XS)) | |
| head(cons(X, XS)) | → | X | tail(cons(X, XS)) | → | XS |
Termination of terms over the following signature is verified: nats, 0, pairs, s, incr, head, odds, tail, cons
Context-sensitive strategy:
μ(pairs) = μ(odds#) = μ(odds) = μ(T) = μ(nats) = μ(0) = μ(nats#) = μ(pairs#) = μ(nil) = ∅
μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(head#) = μ(incr) = μ(head) = μ(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(incr(x_1)) | → | T(x_1) |