NO
The TRS could be proven non-terminating. The proof took 756 ms.
The following reduction sequence is a witness for non-termination:
length#(activate(n__zeros)) →* length#(activate(n__zeros))
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor BackwardsNarrowing (1ms).
| | – Problem 3 was processed with processor BackwardsNarrowing (0ms).
| | | – Problem 4 remains open; application of the following processors failed [BackwardsNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms), BackwardsNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (1ms), Propagation (2ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| length#(cons(N, L)) | → | length#(activate(L)) | | and#(tt, X) | → | activate#(X) |
| activate#(n__zeros) | → | zeros# | | length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | and(tt, X) | → | activate(X) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | s(length(activate(L))) |
| zeros | → | n__zeros | | activate(n__zeros) | → | zeros |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, 0, s, zeros, tt, length, n__zeros, cons, and, nil
Strategy
The following SCCs where found
| length#(cons(N, L)) → length#(activate(L)) |
Problem 2: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| length#(cons(N, L)) | → | length#(activate(L)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | and(tt, X) | → | activate(X) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | s(length(activate(L))) |
| zeros | → | n__zeros | | activate(n__zeros) | → | zeros |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, 0, s, tt, zeros, length, n__zeros, nil, and, cons
Strategy
The left-hand side of the rule length
#(cons(
N,
L)) → length
#(activate(
L)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| length#(activate(cons(N, L))) | |
| length#(zeros) | |
Thus, the rule length
#(cons(
N,
L)) → length
#(activate(
L)) is replaced by the following rules:
| length#(zeros) → length#(activate(n__zeros)) | length#(activate(cons(N, L))) → length#(activate(L)) |
Problem 3: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| length#(zeros) | → | length#(activate(n__zeros)) | | length#(activate(cons(N, L))) | → | length#(activate(L)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | and(tt, X) | → | activate(X) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | s(length(activate(L))) |
| zeros | → | n__zeros | | activate(n__zeros) | → | zeros |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, 0, s, zeros, tt, length, n__zeros, cons, and, nil
Strategy
The left-hand side of the rule length
#(zeros) → length
#(activate(n__zeros)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| length#(activate(zeros)) | |
| length#(activate(n__zeros)) | |
Thus, the rule length
#(zeros) → length
#(activate(n__zeros)) is replaced by the following rules:
| length#(activate(zeros)) → length#(activate(n__zeros)) | length#(activate(n__zeros)) → length#(activate(n__zeros)) |