YES

The TRS could be proven terminating. The proof took 17 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__zeros) → zeros#tail#(cons(X, XS)) → activate#(XS)

Rewrite Rules

zeros → cons(0, n__zeros)tail(cons(X, XS)) → activate(XS)
zeros → n__zerosactivate(n__zeros) → zeros
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: activate, 0, zeros, n__zeros, tail, cons

Strategy


There are no SCCs!