YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

2nd#(cons(X, X1)) → 2nd#(cons1(X, activate(X1)))activate#(n__from(X)) → from#(X)
2nd#(cons(X, X1)) → activate#(X1)

Rewrite Rules

2nd(cons1(X, cons(Y, Z))) → Y2nd(cons(X, X1)) → 2nd(cons1(X, activate(X1)))
from(X) → cons(X, n__from(s(X)))from(X) → n__from(X)
activate(n__from(X)) → from(X)activate(X) → X

Original Signature

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

Strategy

There are no SCCs!