YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (168ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (1245ms).
 |    | – Problem 6 was processed with processor DependencyGraph (1ms).
 |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (11ms).
 |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (9ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (19ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

sqr#(s(X))add#(sqr(X), dbl(X))sqr#(s(X))s#(add(sqr(X), dbl(X)))
activate#(n__s(X))activate#(X)dbl#(s(X))dbl#(X)
dbl#(s(X))s#(dbl(X))add#(s(X), Y)s#(add(X, Y))
terms#(N)sqr#(N)sqr#(s(X))sqr#(X)
activate#(n__first(X1, X2))activate#(X2)activate#(n__first(X1, X2))first#(activate(X1), activate(X2))
activate#(n__first(X1, X2))activate#(X1)add#(s(X), Y)add#(X, Y)
activate#(n__terms(X))activate#(X)first#(s(X), cons(Y, Z))activate#(Z)
dbl#(s(X))s#(s(dbl(X)))activate#(n__terms(X))terms#(activate(X))
sqr#(s(X))dbl#(X)activate#(n__s(X))s#(activate(X))

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


The following SCCs where found

add#(s(X), Y) → add#(X, Y)

dbl#(s(X)) → dbl#(X)

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

sqr#(s(X)) → sqr#(X)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

first(X1, X2)n__first(X1, X2)terms(X)n__terms(X)
s(X)n__s(X)activate(X)X
activate(n__terms(X))terms(activate(X))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))
activate(n__s(X))s(activate(X))activate(n__first(X1, X2))first(activate(X1), activate(X2))

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

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

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, cons, nil

Strategy


The following SCCs where found

activate#(n__terms(X)) → activate#(X)activate#(n__s(X)) → activate#(X)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__terms(X))activate#(X)activate#(n__s(X))activate#(X)

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, cons, nil

Strategy


Polynomial Interpretation

There are no usable rules

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

activate#(n__terms(X))activate#(X)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__s(X))activate#(X)

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


Polynomial Interpretation

There are no usable rules

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

activate#(n__s(X))activate#(X)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

dbl#(s(X))dbl#(X)

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

dbl#(s(X))dbl#(X)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

sqr#(s(X))sqr#(X)

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sqr#(s(X))sqr#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

add#(s(X), Y)add#(X, Y)

Rewrite Rules

terms(N)cons(recip(sqr(N)), n__terms(n__s(N)))sqr(0)0
sqr(s(X))s(add(sqr(X), dbl(X)))dbl(0)0
dbl(s(X))s(s(dbl(X)))add(0, X)X
add(s(X), Y)s(add(X, Y))first(0, X)nil
first(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))terms(X)n__terms(X)
s(X)n__s(X)first(X1, X2)n__first(X1, X2)
activate(n__terms(X))terms(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: terms, sqr, dbl, recip, n__terms, add, n__s, activate, 0, s, n__first, first, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

add#(s(X), Y)add#(X, Y)