YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (81ms).
 | – Problem 2 was processed with processor SubtermCriterion (18ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (350ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (427ms).
 |    |    | – Problem 5 was processed with processor DependencyGraph (4ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__first(X1, X2))first#(activate(X1), activate(X2))activate#(n__first(X1, X2))activate#(X1)
first#(s(X), cons(Y, Z))activate#(Z)sel#(s(X), cons(Y, Z))activate#(Z)
activate#(n__from(X))from#(activate(X))activate#(n__s(X))activate#(X)
activate#(n__from(X))activate#(X)activate#(n__s(X))s#(activate(X))
sel#(s(X), cons(Y, Z))sel#(X, activate(Z))activate#(n__first(X1, X2))activate#(X2)

Rewrite Rules

from(X)cons(X, n__from(n__s(X)))first(0, Z)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))sel(0, cons(X, Z))X
sel(s(X), cons(Y, Z))sel(X, activate(Z))from(X)n__from(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__s, activate, 0, n__from, s, n__first, from, first, sel, cons, nil

Strategy


The following SCCs where found

activate#(n__first(X1, X2)) → first#(activate(X1), activate(X2))activate#(n__first(X1, X2)) → activate#(X1)
first#(s(X), cons(Y, Z)) → activate#(Z)activate#(n__s(X)) → activate#(X)
activate#(n__from(X)) → activate#(X)activate#(n__first(X1, X2)) → activate#(X2)

sel#(s(X), cons(Y, Z)) → sel#(X, activate(Z))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

sel#(s(X), cons(Y, Z))sel#(X, activate(Z))

Rewrite Rules

from(X)cons(X, n__from(n__s(X)))first(0, Z)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))sel(0, cons(X, Z))X
sel(s(X), cons(Y, Z))sel(X, activate(Z))from(X)n__from(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__s, activate, 0, n__from, s, n__first, from, first, sel, cons, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sel#(s(X), cons(Y, Z))sel#(X, activate(Z))

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__first(X1, X2))first#(activate(X1), activate(X2))activate#(n__first(X1, X2))activate#(X1)
first#(s(X), cons(Y, Z))activate#(Z)activate#(n__s(X))activate#(X)
activate#(n__from(X))activate#(X)activate#(n__first(X1, X2))activate#(X2)

Rewrite Rules

from(X)cons(X, n__from(n__s(X)))first(0, Z)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))sel(0, cons(X, Z))X
sel(s(X), cons(Y, Z))sel(X, activate(Z))from(X)n__from(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__s, activate, 0, n__from, s, n__first, from, first, sel, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

first(X1, X2)n__first(X1, X2)from(X)cons(X, n__from(n__s(X)))
s(X)n__s(X)activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))first(0, Z)nil

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__from(X))activate#(X)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__first(X1, X2))first#(activate(X1), activate(X2))activate#(n__first(X1, X2))activate#(X1)
first#(s(X), cons(Y, Z))activate#(Z)activate#(n__s(X))activate#(X)
activate#(n__first(X1, X2))activate#(X2)

Rewrite Rules

from(X)cons(X, n__from(n__s(X)))first(0, Z)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))sel(0, cons(X, Z))X
sel(s(X), cons(Y, Z))sel(X, activate(Z))from(X)n__from(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__s, 0, s, n__from, n__first, from, sel, first, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

first(X1, X2)n__first(X1, X2)from(X)cons(X, n__from(n__s(X)))
s(X)n__s(X)activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))first(0, Z)nil

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__first(X1, X2))first#(activate(X1), activate(X2))activate#(n__first(X1, X2))activate#(X1)
activate#(n__s(X))activate#(X)activate#(n__first(X1, X2))activate#(X2)

Problem 5: DependencyGraph



Dependency Pair Problem

Dependency Pairs

first#(s(X), cons(Y, Z))activate#(Z)

Rewrite Rules

from(X)cons(X, n__from(n__s(X)))first(0, Z)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))sel(0, cons(X, Z))X
sel(s(X), cons(Y, Z))sel(X, activate(Z))from(X)n__from(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__first(X1, X2))first(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__s, activate, 0, n__from, s, n__first, from, first, sel, cons, nil

Strategy


There are no SCCs!