The TRS could be proven non-terminating. The proof took 319 ms.
The following reduction sequence is a witness for non-termination:
nats# →* nats#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)].
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) |
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)) | → | X | tail(cons(X, XS)) | → | activate(XS) | |
incr(X) | → | n__incr(X) | activate(n__incr(X)) | → | incr(X) | |
activate(X) | → | X |
Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons
nats# → nats# |
odds# → pairs# | pairs# → odds# |
incr#(cons(X, XS)) → activate#(XS) | activate#(n__incr(X)) → incr#(X) |
odds# | → | pairs# | pairs# | → | odds# |
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)) | → | X | tail(cons(X, XS)) | → | activate(XS) | |
incr(X) | → | n__incr(X) | activate(n__incr(X)) | → | incr(X) | |
activate(X) | → | X |
Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons
This is possible as
This is possible as
This is possible as
This is possible as
Removed Dependency Pairs | Added Dependency Pairs |
---|---|
odds# → pairs# | pairs# → pairs# |
pairs# → odds# | odds# → odds# |
incr#(cons(X, XS)) | → | activate#(XS) | activate#(n__incr(X)) | → | incr#(X) |
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)) | → | X | tail(cons(X, XS)) | → | activate(XS) | |
incr(X) | → | n__incr(X) | activate(n__incr(X)) | → | incr(X) | |
activate(X) | → | X |
Termination of terms over the following signature is verified: activate, n__incr, nats, 0, pairs, s, incr, head, odds, tail, cons
The following projection was used:
Thus, the following dependency pairs are removed:
incr#(cons(X, XS)) | → | activate#(XS) | activate#(n__incr(X)) | → | incr#(X) |