NO

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

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

nats# →* nats#

The following DP Processors were used


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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

nats# → nats#odds# → pairs#
pairs# → odds#incr#(cons(X, XS)) → activate#(XS)
activate#(n__incr(X)) → incr#(X)odds# → incr#(pairs)
tail#(cons(X, XS)) → activate#(XS)

Rewrite Rules

nats → cons(0, n__incr(nats))pairs → cons(0, n__incr(odds))
odds → incr(pairs)incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
head(cons(X, XS)) → Xtail(cons(X, XS)) → activate(XS)
incr(X) → n__incr(X)activate(n__incr(X)) → incr(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons

Strategy

The following SCCs where found

nats# → nats#
odds# → pairs#pairs# → odds#
incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → incr#(X)

Problem 2: Propagation

Dependency Pair Problem

Dependency Pairs

odds# → pairs#pairs# → odds#

Rewrite Rules

nats → cons(0, n__incr(nats))pairs → cons(0, n__incr(odds))
odds → incr(pairs)incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
head(cons(X, XS)) → Xtail(cons(X, XS)) → activate(XS)
incr(X) → n__incr(X)activate(n__incr(X)) → incr(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons

Strategy

The dependency pairs odds# → pairs# and pairs# → odds# are consolidated into the rule odds# → odds# .

This is possible as

The dependency pairs odds# → pairs# and pairs# → odds# are consolidated into the rule odds# → odds# .

This is possible as

The dependency pairs pairs# → odds# and odds# → pairs# are consolidated into the rule pairs# → pairs# .

This is possible as

The dependency pairs pairs# → odds# and odds# → pairs# are consolidated into the rule pairs# → pairs# .

This is possible as

Summary

Removed Dependency PairsAdded Dependency Pairs
odds# → pairs#pairs# → pairs#
pairs# → odds#odds# → odds#

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → incr#(X)

Rewrite Rules

nats → cons(0, n__incr(nats))pairs → cons(0, n__incr(odds))
odds → incr(pairs)incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
head(cons(X, XS)) → Xtail(cons(X, XS)) → activate(XS)
incr(X) → n__incr(X)activate(n__incr(X)) → incr(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → incr#(X)