NO

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

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

pairNs# →* pairNs#

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (189ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (203ms).
 |    | – Problem 4 was processed with processor DependencyGraph (24ms).
 |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (160ms).
 |    |    |    | – Problem 6 was processed with processor DependencyGraph (13ms).
 |    |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (84ms).
 |    |    |    |    |    | – Problem 8 was processed with processor DependencyGraph (6ms).
 |    |    |    |    |    |    | – Problem 9 was processed with processor PolynomialLinearRange4iUR (83ms).
 | – Problem 3 was processed with processor Propagation (3ms).
 |    | – Problem 10 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (3ms), ForwardInstantiation (1ms), Propagation (3ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

incr#(cons(X, XS))cons#(s(X), n__incr(activate(XS)))oddNs#incr#(pairNs)
zip#(cons(X, XS), cons(Y, YS))cons#(pair(X, Y), n__zip(activate(XS), activate(YS)))incr#(cons(X, XS))activate#(XS)
activate#(n__incr(X))incr#(X)pairNs#cons#(0, n__incr(oddNs))
tail#(cons(X, XS))activate#(XS)take#(s(N), cons(X, XS))activate#(XS)
activate#(n__repItems(X))repItems#(X)zip#(cons(X, XS), cons(Y, YS))activate#(XS)
repItems#(cons(X, XS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
pairNs#oddNs#oddNs#pairNs#
activate#(n__take(X1, X2))take#(X1, X2)take#(s(N), cons(X, XS))cons#(X, n__take(N, activate(XS)))
activate#(n__cons(X1, X2))cons#(X1, X2)repItems#(cons(X, XS))cons#(X, n__cons(X, n__repItems(activate(XS))))
activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons

Strategy


The following SCCs where found

pairNs# → oddNs#oddNs# → pairNs#

take#(s(N), cons(X, XS)) → activate#(XS)activate#(n__repItems(X)) → repItems#(X)
zip#(cons(X, XS), cons(Y, YS)) → activate#(XS)repItems#(cons(X, XS)) → activate#(XS)
zip#(cons(X, XS), cons(Y, YS)) → activate#(YS)incr#(cons(X, XS)) → activate#(XS)
activate#(n__take(X1, X2)) → take#(X1, X2)activate#(n__incr(X)) → incr#(X)
activate#(n__zip(X1, X2)) → zip#(X1, X2)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

take#(s(N), cons(X, XS))activate#(XS)activate#(n__repItems(X))repItems#(X)
zip#(cons(X, XS), cons(Y, YS))activate#(XS)repItems#(cons(X, XS))activate#(XS)
zip#(cons(X, XS), cons(Y, YS))activate#(YS)incr#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))take#(X1, X2)activate#(n__incr(X))incr#(X)
activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons

Strategy


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:

repItems#(cons(X, XS))activate#(XS)

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

take#(s(N), cons(X, XS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(XS)
activate#(n__repItems(X))repItems#(X)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
incr#(cons(X, XS))activate#(XS)activate#(n__take(X1, X2))take#(X1, X2)
activate#(n__incr(X))incr#(X)activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


The following SCCs where found

take#(s(N), cons(X, XS)) → activate#(XS)zip#(cons(X, XS), cons(Y, YS)) → activate#(XS)
zip#(cons(X, XS), cons(Y, YS)) → activate#(YS)incr#(cons(X, XS)) → activate#(XS)
activate#(n__take(X1, X2)) → take#(X1, X2)activate#(n__incr(X)) → incr#(X)
activate#(n__zip(X1, X2)) → zip#(X1, X2)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

take#(s(N), cons(X, XS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(XS)
zip#(cons(X, XS), cons(Y, YS))activate#(YS)incr#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))take#(X1, X2)activate#(n__incr(X))incr#(X)
activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


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:

take#(s(N), cons(X, XS))activate#(XS)

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zip#(cons(X, XS), cons(Y, YS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
incr#(cons(X, XS))activate#(XS)activate#(n__take(X1, X2))take#(X1, X2)
activate#(n__incr(X))incr#(X)activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons

Strategy


The following SCCs where found

zip#(cons(X, XS), cons(Y, YS)) → activate#(XS)zip#(cons(X, XS), cons(Y, YS)) → activate#(YS)
incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → incr#(X)
activate#(n__zip(X1, X2)) → zip#(X1, X2)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

zip#(cons(X, XS), cons(Y, YS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))incr#(X)
activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons

Strategy


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:

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

Problem 8: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zip#(cons(X, XS), cons(Y, YS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
activate#(n__incr(X))incr#(X)activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


The following SCCs where found

zip#(cons(X, XS), cons(Y, YS)) → activate#(XS)zip#(cons(X, XS), cons(Y, YS)) → activate#(YS)
activate#(n__zip(X1, X2)) → zip#(X1, X2)

Problem 9: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

zip#(cons(X, XS), cons(Y, YS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
activate#(n__zip(X1, X2))zip#(X1, X2)

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


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:

zip#(cons(X, XS), cons(Y, YS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
activate#(n__zip(X1, X2))zip#(X1, X2)

Problem 3: Propagation



Dependency Pair Problem

Dependency Pairs

pairNs#oddNs#oddNs#pairNs#

Rewrite Rules

pairNscons(0, n__incr(oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
take(X1, X2)n__take(X1, X2)zip(X1, X2)n__zip(X1, X2)
cons(X1, X2)n__cons(X1, X2)repItems(X)n__repItems(X)
activate(n__incr(X))incr(X)activate(n__take(X1, X2))take(X1, X2)
activate(n__zip(X1, X2))zip(X1, X2)activate(n__cons(X1, X2))cons(X1, X2)
activate(n__repItems(X))repItems(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons

Strategy


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

This is possible as

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

This is possible as

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

This is possible as

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

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
pairNs# → oddNs#pairNs# → pairNs#
oddNs# → pairNs#oddNs# → oddNs#