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

zeroscons(0, n__zeros)and(tt, X)activate(X)
length(nil)0length(cons(N, L))s(length(activate(L)))
zerosn__zerosactivate(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

zeroscons(0, n__zeros)and(tt, X)activate(X)
length(nil)0length(cons(N, L))s(length(activate(L)))
zerosn__zerosactivate(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 TermsIrrelevant 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

zeroscons(0, n__zeros)and(tt, X)activate(X)
length(nil)0length(cons(N, L))s(length(activate(L)))
zerosn__zerosactivate(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 TermsIrrelevant 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))