The TRS could be proven non-terminating. The proof took 197 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 (0ms).
| – Problem 2 was processed with processor SubtermCriterion (0ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (2ms), SubtermCriterion (1ms), DependencyGraph (1ms), PolynomialOrdering (29ms), DependencyGraph (1ms), PolynomialOrdering (27ms), DependencyGraph (1ms), PolynomialOrdering (14ms), DependencyGraph (1ms), ReductionPairSAT (16ms), DependencyGraph (1ms), SizeChangePrinciple (1ms), BackwardsNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (3ms), Propagation (3ms)].
| – Problem 4 was processed with processor SubtermCriterion (0ms).
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
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
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 4: 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) |