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) | → | nil | | incr(cons(X, L)) | → | cons(s(X), incr(L)) |
| adx(nil) | → | nil | | adx(cons(X, L)) | → | incr(cons(X, adx(L))) |
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| head(cons(X, L)) | → | X | | tail(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) |
| adx#(cons(X, L)) → adx#(L) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| incr#(cons(X, L)) | → | incr#(L) |
Rewrite Rules
| incr(nil) | → | nil | | incr(cons(X, L)) | → | cons(s(X), incr(L)) |
| adx(nil) | → | nil | | adx(cons(X, L)) | → | incr(cons(X, adx(L))) |
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| head(cons(X, L)) | → | X | | tail(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) | → | nil | | incr(cons(X, L)) | → | cons(s(X), incr(L)) |
| adx(nil) | → | nil | | adx(cons(X, L)) | → | incr(cons(X, adx(L))) |
| nats | → | adx(zeros) | | zeros | → | cons(0, zeros) |
| head(cons(X, L)) | → | X | | tail(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) |