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 (6ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

from#(X) → cons#(X, n__from(s(X)))2nd#(cons(X, n__cons(Y, Z))) → activate#(Y)
activate#(n__from(X)) → from#(X)activate#(n__cons(X1, X2)) → cons#(X1, X2)

Rewrite Rules

2nd(cons(X, n__cons(Y, Z))) → activate(Y)from(X) → cons(X, n__from(s(X)))
cons(X1, X2) → n__cons(X1, X2)from(X) → n__from(X)
activate(n__cons(X1, X2)) → cons(X1, X2)activate(n__from(X)) → from(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: activate, 2nd, n__cons, s, n__from, from, cons

Strategy

There are no SCCs!