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