YES

The TRS could be proven terminating. The proof took 235 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (37ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (72ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (15ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (16ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(adx(Y)) → adx#(Y)T(zeros) → zeros#
T(incr(x_1)) → T(x_1)T(s(x_1)) → T(x_1)
nats# → zeros#hd#(cons(X, Y)) → T(X)
T(adx(x_1)) → T(x_1)tl#(cons(X, Y)) → T(Y)
adx#(cons(X, Y)) → incr#(cons(X, adx(Y)))T(incr(Y)) → incr#(Y)
nats# → adx#(zeros)

Rewrite Rules

nats → adx(zeros)zeros → cons(0, zeros)
incr(cons(X, Y)) → cons(s(X), incr(Y))adx(cons(X, Y)) → incr(cons(X, adx(Y)))
hd(cons(X, Y)) → Xtl(cons(X, Y)) → Y

Original Signature

Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(s) = μ(zeros) = μ(nats#) = μ(cons) = ∅
μ(adx#) = μ(tl) = μ(hd) = μ(incr#) = μ(hd#) = μ(adx) = μ(incr) = μ(tl#) = {1}

The following SCCs where found

T(incr(x_1)) → T(x_1)T(s(x_1)) → T(x_1)
T(adx(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(incr(x_1)) → T(x_1)T(s(x_1)) → T(x_1)
T(adx(x_1)) → T(x_1)

Rewrite Rules

nats → adx(zeros)zeros → cons(0, zeros)
incr(cons(X, Y)) → cons(s(X), incr(Y))adx(cons(X, Y)) → incr(cons(X, adx(Y)))
hd(cons(X, Y)) → Xtl(cons(X, Y)) → Y

Original Signature

Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(s) = μ(zeros) = μ(nats#) = μ(cons) = ∅
μ(adx#) = μ(tl) = μ(hd) = μ(incr#) = μ(hd#) = μ(adx) = μ(incr) = μ(tl#) = {1}

Polynomial Interpretation

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)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(s(x_1)) → T(x_1)T(adx(x_1)) → T(x_1)

Rewrite Rules

nats → adx(zeros)zeros → cons(0, zeros)
incr(cons(X, Y)) → cons(s(X), incr(Y))adx(cons(X, Y)) → incr(cons(X, adx(Y)))
hd(cons(X, Y)) → Xtl(cons(X, Y)) → Y

Original Signature

Termination of terms over the following signature is verified: nats, tl, 0, s, zeros, adx, hd, incr, cons

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(s) = μ(zeros) = μ(nats#) = μ(cons) = ∅
μ(adx#) = μ(tl) = μ(hd) = μ(incr#) = μ(hd#) = μ(adx) = μ(incr) = μ(tl#) = {1}

Polynomial Interpretation

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)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(s(x_1)) → T(x_1)

Rewrite Rules

nats → adx(zeros)zeros → cons(0, zeros)
incr(cons(X, Y)) → cons(s(X), incr(Y))adx(cons(X, Y)) → incr(cons(X, adx(Y)))
hd(cons(X, Y)) → Xtl(cons(X, Y)) → Y

Original Signature

Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(s) = μ(zeros) = μ(nats#) = μ(cons) = ∅
μ(adx#) = μ(tl) = μ(hd) = μ(incr#) = μ(hd#) = μ(adx) = μ(incr) = μ(tl#) = {1}

Polynomial Interpretation

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)