YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (24ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (50ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (27ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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)

Rewrite Rules

incr(nil)nilincr(cons(X, L))cons(s(X), incr(L))
adx(nil)niladx(cons(X, L))incr(cons(X, adx(L)))
natsadx(zeros)zeroscons(0, zeros)
head(cons(X, L))Xtail(cons(X, L))L

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, adx, incr, head, tail, nil, cons

Strategy

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


The following SCCs where found

T(incr(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(adx(x_1))T(x_1)

Rewrite Rules

incr(nil)nilincr(cons(X, L))cons(s(X), incr(L))
adx(nil)niladx(cons(X, L))incr(cons(X, adx(L)))
natsadx(zeros)zeroscons(0, zeros)
head(cons(X, L))Xtail(cons(X, L))L

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, adx, incr, head, tail, nil, cons

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(zeros) = μ(nats#) = μ(nil) = ∅
μ(adx#) = μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(adx) = μ(head#) = μ(incr) = μ(head) = μ(cons) = {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(adx(x_1))T(x_1)

Rewrite Rules

incr(nil)nilincr(cons(X, L))cons(s(X), incr(L))
adx(nil)niladx(cons(X, L))incr(cons(X, adx(L)))
natsadx(zeros)zeroscons(0, zeros)
head(cons(X, L))Xtail(cons(X, L))L

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, adx, incr, head, tail, cons, nil

Strategy

Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(nats) = μ(0) = μ(zeros) = μ(nats#) = μ(nil) = ∅
μ(adx#) = μ(incr#) = μ(tail#) = μ(tail) = μ(s) = μ(adx) = μ(head#) = μ(incr) = μ(head) = μ(cons) = {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)