NO

The TRS could be proven non-terminating. The proof took 259 ms.

The following reduction sequence is a witness for non-termination:

zeros# →* zeros#

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (26ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (74ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (64ms), DependencyGraph (1ms), ReductionPairSAT (14ms), DependencyGraph (1ms), SizeChangePrinciple (1ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

incr#(cons(X, L))incr#(L)nats#zeros#
adx#(cons(X, L))incr#(cons(X, adx(L)))zeros#zeros#
adx#(cons(X, L))adx#(L)nats#adx#(zeros)

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


The following SCCs where found

incr#(cons(X, L)) → incr#(L)

zeros# → zeros#

adx#(cons(X, L)) → adx#(L)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

incr#(cons(X, L))incr#(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


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

incr#(cons(X, L))incr#(L)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

adx#(cons(X, 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


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

adx#(cons(X, L))adx#(L)