NO
The TRS could be proven non-terminating. The proof took 274 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 (25ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (46ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (27ms), DependencyGraph (1ms), ReductionPairSAT (15ms), DependencyGraph (0ms), SizeChangePrinciple (1ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| nats# | → | zeros# | | adx#(cons(X, Y)) | → | incr#(cons(X, adx(Y))) |
| zeros# | → | zeros# | | incr#(cons(X, Y)) | → | incr#(Y) |
| adx#(cons(X, Y)) | → | adx#(Y) | | nats# | → | adx#(zeros) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| incr(cons(X, Y)) | → | cons(s(X), incr(Y)) | | adx(cons(X, Y)) | → | incr(cons(X, adx(Y))) |
| hd(cons(X, Y)) | → | X | | tl(cons(X, Y)) | → | Y |
Original Signature
Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons
Strategy
The following SCCs where found
| incr#(cons(X, Y)) → incr#(Y) |
| adx#(cons(X, Y)) → adx#(Y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| incr#(cons(X, Y)) | → | incr#(Y) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| incr(cons(X, Y)) | → | cons(s(X), incr(Y)) | | adx(cons(X, Y)) | → | incr(cons(X, adx(Y))) |
| hd(cons(X, Y)) | → | X | | tl(cons(X, Y)) | → | Y |
Original Signature
Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| incr#(cons(X, Y)) | → | incr#(Y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| adx#(cons(X, Y)) | → | adx#(Y) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| incr(cons(X, Y)) | → | cons(s(X), incr(Y)) | | adx(cons(X, Y)) | → | incr(cons(X, adx(Y))) |
| hd(cons(X, Y)) | → | X | | tl(cons(X, Y)) | → | Y |
Original Signature
Termination of terms over the following signature is verified: nats, 0, tl, s, zeros, adx, hd, incr, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| adx#(cons(X, Y)) | → | adx#(Y) |