YES
0 QTRS
↳1 DependencyPairsProof (⇔, 13 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 TRUE
2nd(cons1(X, cons(Y, Z))) → Y
2nd(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
2ND(cons(X, X1)) → 2ND(cons1(X, activate(X1)))
2ND(cons(X, X1)) → ACTIVATE(X1)
ACTIVATE(n__from(X)) → FROM(X)
2nd(cons1(X, cons(Y, Z))) → Y
2nd(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