YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (185ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (1444ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (753ms).
 |    |    | – Problem 4 was processed with processor DependencyGraph (9ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (602ms).
 |    |    |    |    | – Problem 6 was processed with processor DependencyGraph (4ms).
 |    |    |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (258ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__add(X1, X2))activate#(X2)add#(s(X), Y)activate#(X)
activate#(n__fst(X1, X2))activate#(X2)activate#(n__from(X))activate#(X)
activate#(n__len(X))len#(activate(X))activate#(n__s(X))s#(X)
add#(s(X), Y)s#(n__add(activate(X), Y))activate#(n__add(X1, X2))activate#(X1)
activate#(n__len(X))activate#(X)len#(cons(X, Z))s#(n__len(activate(Z)))
activate#(n__from(X))from#(activate(X))len#(cons(X, Z))activate#(Z)
activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2))activate#(X1)
activate#(n__add(X1, X2))add#(activate(X1), activate(X2))fst#(s(X), cons(Y, Z))activate#(Z)
fst#(s(X), cons(Y, Z))activate#(X)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, cons, nil

Strategy


The following SCCs where found

activate#(n__add(X1, X2)) → activate#(X2)activate#(n__fst(X1, X2)) → activate#(X2)
add#(s(X), Y) → activate#(X)activate#(n__from(X)) → activate#(X)
activate#(n__len(X)) → len#(activate(X))activate#(n__add(X1, X2)) → activate#(X1)
activate#(n__len(X)) → activate#(X)len#(cons(X, Z)) → activate#(Z)
activate#(n__fst(X1, X2)) → fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2)) → activate#(X1)
activate#(n__add(X1, X2)) → add#(activate(X1), activate(X2))fst#(s(X), cons(Y, Z)) → activate#(X)
fst#(s(X), cons(Y, Z)) → activate#(Z)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

add#(s(X), Y)activate#(X)activate#(n__fst(X1, X2))activate#(X2)
activate#(n__add(X1, X2))activate#(X2)activate#(n__from(X))activate#(X)
activate#(n__len(X))len#(activate(X))activate#(n__add(X1, X2))activate#(X1)
activate#(n__len(X))activate#(X)len#(cons(X, Z))activate#(Z)
activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2))activate#(X1)
activate#(n__add(X1, X2))add#(activate(X1), activate(X2))fst#(s(X), cons(Y, Z))activate#(Z)
fst#(s(X), cons(Y, Z))activate#(X)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

from(X)cons(X, n__from(n__s(X)))len(X)n__len(X)
len(cons(X, Z))s(n__len(activate(Z)))activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__s(X))s(X)
add(0, X)Xadd(X1, X2)n__add(X1, X2)
len(nil)0fst(0, Z)nil
fst(X1, X2)n__fst(X1, X2)s(X)n__s(X)
activate(n__len(X))len(activate(X))activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
fst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))add(s(X), Y)s(n__add(activate(X), Y))

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 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__add(X1, X2))activate#(X1)activate#(n__len(X))activate#(X)
activate#(n__add(X1, X2))activate#(X2)activate#(n__fst(X1, X2))activate#(X2)
add#(s(X), Y)activate#(X)len#(cons(X, Z))activate#(Z)
activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2))activate#(X1)
activate#(n__add(X1, X2))add#(activate(X1), activate(X2))activate#(n__len(X))len#(activate(X))
fst#(s(X), cons(Y, Z))activate#(X)fst#(s(X), cons(Y, Z))activate#(Z)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

from(X)cons(X, n__from(n__s(X)))len(X)n__len(X)
len(cons(X, Z))s(n__len(activate(Z)))activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__s(X))s(X)
add(0, X)Xadd(X1, X2)n__add(X1, X2)
len(nil)0fst(0, Z)nil
fst(X1, X2)n__fst(X1, X2)s(X)n__s(X)
activate(n__len(X))len(activate(X))activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
fst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))add(s(X), Y)s(n__add(activate(X), Y))

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

activate#(n__len(X))activate#(X)len#(cons(X, Z))activate#(Z)

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__add(X1, X2))activate#(X1)add#(s(X), Y)activate#(X)
activate#(n__fst(X1, X2))activate#(X2)activate#(n__add(X1, X2))activate#(X2)
activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2))activate#(X1)
activate#(n__len(X))len#(activate(X))activate#(n__add(X1, X2))add#(activate(X1), activate(X2))
fst#(s(X), cons(Y, Z))activate#(Z)fst#(s(X), cons(Y, Z))activate#(X)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, cons, nil

Strategy


The following SCCs where found

activate#(n__add(X1, X2)) → activate#(X1)activate#(n__fst(X1, X2)) → activate#(X2)
add#(s(X), Y) → activate#(X)activate#(n__add(X1, X2)) → activate#(X2)
activate#(n__fst(X1, X2)) → fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2)) → activate#(X1)
activate#(n__add(X1, X2)) → add#(activate(X1), activate(X2))fst#(s(X), cons(Y, Z)) → activate#(Z)
fst#(s(X), cons(Y, Z)) → activate#(X)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__add(X1, X2))activate#(X1)activate#(n__fst(X1, X2))activate#(X2)
add#(s(X), Y)activate#(X)activate#(n__add(X1, X2))activate#(X2)
activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))activate#(n__fst(X1, X2))activate#(X1)
activate#(n__add(X1, X2))add#(activate(X1), activate(X2))fst#(s(X), cons(Y, Z))activate#(Z)
fst#(s(X), cons(Y, Z))activate#(X)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

from(X)cons(X, n__from(n__s(X)))len(X)n__len(X)
len(cons(X, Z))s(n__len(activate(Z)))activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__s(X))s(X)
add(0, X)Xadd(X1, X2)n__add(X1, X2)
len(nil)0fst(0, Z)nil
fst(X1, X2)n__fst(X1, X2)s(X)n__s(X)
activate(n__len(X))len(activate(X))activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
fst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))add(s(X), Y)s(n__add(activate(X), Y))

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

activate#(n__add(X1, X2))activate#(X1)activate#(n__add(X1, X2))activate#(X2)
add#(s(X), Y)activate#(X)

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__fst(X1, X2))activate#(X2)activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))
activate#(n__fst(X1, X2))activate#(X1)activate#(n__add(X1, X2))add#(activate(X1), activate(X2))
fst#(s(X), cons(Y, Z))activate#(X)fst#(s(X), cons(Y, Z))activate#(Z)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, nil, cons

Strategy


The following SCCs where found

activate#(n__fst(X1, X2)) → activate#(X2)activate#(n__fst(X1, X2)) → fst#(activate(X1), activate(X2))
activate#(n__fst(X1, X2)) → activate#(X1)fst#(s(X), cons(Y, Z)) → activate#(Z)
fst#(s(X), cons(Y, Z)) → activate#(X)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__fst(X1, X2))activate#(X2)activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))
activate#(n__fst(X1, X2))activate#(X1)fst#(s(X), cons(Y, Z))activate#(Z)
fst#(s(X), cons(Y, Z))activate#(X)

Rewrite Rules

fst(0, Z)nilfst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))
from(X)cons(X, n__from(n__s(X)))add(0, X)X
add(s(X), Y)s(n__add(activate(X), Y))len(nil)0
len(cons(X, Z))s(n__len(activate(Z)))fst(X1, X2)n__fst(X1, X2)
from(X)n__from(X)s(X)n__s(X)
add(X1, X2)n__add(X1, X2)len(X)n__len(X)
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__from(X))from(activate(X))
activate(n__s(X))s(X)activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__len(X))len(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__from, from, len, n__len, add, n__fst, fst, activate, n__s, 0, s, n__add, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

from(X)cons(X, n__from(n__s(X)))len(X)n__len(X)
len(cons(X, Z))s(n__len(activate(Z)))activate(n__add(X1, X2))add(activate(X1), activate(X2))
activate(n__fst(X1, X2))fst(activate(X1), activate(X2))activate(n__s(X))s(X)
add(0, X)Xadd(X1, X2)n__add(X1, X2)
len(nil)0fst(0, Z)nil
fst(X1, X2)n__fst(X1, X2)s(X)n__s(X)
activate(n__len(X))len(activate(X))activate(X)X
from(X)n__from(X)activate(n__from(X))from(activate(X))
fst(s(X), cons(Y, Z))cons(Y, n__fst(activate(X), activate(Z)))add(s(X), Y)s(n__add(activate(X), Y))

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

activate#(n__fst(X1, X2))activate#(X2)activate#(n__fst(X1, X2))fst#(activate(X1), activate(X2))
activate#(n__fst(X1, X2))activate#(X1)fst#(s(X), cons(Y, Z))activate#(X)
fst#(s(X), cons(Y, Z))activate#(Z)