YES
The TRS could be proven terminating. The proof took 2265 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (158ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (1511ms).
| | – Problem 3 was processed with processor DependencyGraph (6ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (31ms).
| | | | – Problem 6 was processed with processor DependencyGraph (0ms).
| | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (464ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| sqr#(s(X)) | → | sqr#(activate(X)) | | dbl#(s(X)) | → | s#(n__s(n__dbl(activate(X)))) |
| sqr#(s(X)) | → | dbl#(activate(X)) | | dbl#(s(X)) | → | activate#(X) |
| add#(s(X), Y) | → | activate#(X) | | terms#(N) | → | sqr#(N) |
| sqr#(s(X)) | → | s#(n__add(sqr(activate(X)), dbl(activate(X)))) | | activate#(n__s(X)) | → | s#(X) |
| first#(s(X), cons(Y, Z)) | → | activate#(X) | | terms#(N) | → | s#(N) |
| activate#(n__add(X1, X2)) | → | add#(X1, X2) | | add#(s(X), Y) | → | s#(n__add(activate(X), Y)) |
| activate#(n__terms(X)) | → | terms#(X) | | first#(s(X), cons(Y, Z)) | → | activate#(Z) |
| activate#(n__dbl(X)) | → | dbl#(X) | | sqr#(s(X)) | → | activate#(X) |
| activate#(n__first(X1, X2)) | → | first#(X1, X2) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, n__dbl, first, cons, nil
Strategy
The following SCCs where found
| activate#(n__add(X1, X2)) → add#(X1, X2) | activate#(n__terms(X)) → terms#(X) |
| sqr#(s(X)) → sqr#(activate(X)) | sqr#(s(X)) → dbl#(activate(X)) |
| first#(s(X), cons(Y, Z)) → activate#(Z) | activate#(n__dbl(X)) → dbl#(X) |
| dbl#(s(X)) → activate#(X) | add#(s(X), Y) → activate#(X) |
| sqr#(s(X)) → activate#(X) | activate#(n__first(X1, X2)) → first#(X1, X2) |
| terms#(N) → sqr#(N) | first#(s(X), cons(Y, Z)) → activate#(X) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__add(X1, X2)) | → | add#(X1, X2) | | activate#(n__terms(X)) | → | terms#(X) |
| sqr#(s(X)) | → | sqr#(activate(X)) | | first#(s(X), cons(Y, Z)) | → | activate#(Z) |
| sqr#(s(X)) | → | dbl#(activate(X)) | | activate#(n__dbl(X)) | → | dbl#(X) |
| sqr#(s(X)) | → | activate#(X) | | dbl#(s(X)) | → | activate#(X) |
| add#(s(X), Y) | → | activate#(X) | | activate#(n__first(X1, X2)) | → | first#(X1, X2) |
| terms#(N) | → | sqr#(N) | | first#(s(X), cons(Y, Z)) | → | activate#(X) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, n__dbl, first, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): 2x
- activate#(x): 2x
- add(x,y): 2y + 2x
- add#(x,y): x
- cons(x,y): y + 1
- dbl(x): 2x
- dbl#(x): x
- first(x,y): 2y + x + 1
- first#(x,y): 2y + 2x
- n__add(x,y): y + x
- n__dbl(x): x
- n__first(x,y): y + x + 1
- n__s(x): x
- n__terms(x): x + 1
- nil: 1
- recip(x): 2x + 3
- s(x): 2x
- sqr(x): 0
- sqr#(x): x + 2
- terms(x): 2x + 2
- terms#(x): 2x + 2
Improved Usable rules
| first(X1, X2) | → | n__first(X1, X2) | | terms(X) | → | n__terms(X) |
| activate(n__add(X1, X2)) | → | add(X1, X2) | | terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) |
| activate(n__s(X)) | → | s(X) | | dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) |
| add(0, X) | → | X | | first(0, X) | → | nil |
| add(X1, X2) | → | n__add(X1, X2) | | activate(n__terms(X)) | → | terms(X) |
| dbl(0) | → | 0 | | first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) |
| s(X) | → | n__s(X) | | activate(n__first(X1, X2)) | → | first(X1, X2) |
| activate(X) | → | X | | dbl(X) | → | n__dbl(X) |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | activate(n__dbl(X)) | → | dbl(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sqr#(s(X)) | → | dbl#(activate(X)) | | first#(s(X), cons(Y, Z)) | → | activate#(X) |
| first#(s(X), cons(Y, Z)) | → | activate#(Z) | | sqr#(s(X)) | → | activate#(X) |
| activate#(n__first(X1, X2)) | → | first#(X1, X2) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__add(X1, X2)) | → | add#(X1, X2) | | sqr#(s(X)) | → | sqr#(activate(X)) |
| activate#(n__terms(X)) | → | terms#(X) | | activate#(n__dbl(X)) | → | dbl#(X) |
| add#(s(X), Y) | → | activate#(X) | | dbl#(s(X)) | → | activate#(X) |
| terms#(N) | → | sqr#(N) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, first, n__dbl, nil, cons
Strategy
The following SCCs where found
| sqr#(s(X)) → sqr#(activate(X)) |
| activate#(n__add(X1, X2)) → add#(X1, X2) | activate#(n__dbl(X)) → dbl#(X) |
| add#(s(X), Y) → activate#(X) | dbl#(s(X)) → activate#(X) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__add(X1, X2)) | → | add#(X1, X2) | | activate#(n__dbl(X)) | → | dbl#(X) |
| add#(s(X), Y) | → | activate#(X) | | dbl#(s(X)) | → | activate#(X) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, first, n__dbl, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): 0
- activate#(x): x
- add(x,y): 0
- add#(x,y): x + 1
- cons(x,y): 0
- dbl(x): 0
- dbl#(x): x
- first(x,y): 0
- n__add(x,y): x + 1
- n__dbl(x): x + 2
- n__first(x,y): 0
- n__s(x): 0
- n__terms(x): 0
- nil: 0
- recip(x): 0
- s(x): x + 1
- sqr(x): 0
- terms(x): 0
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__dbl(X)) | → | dbl#(X) | | dbl#(s(X)) | → | activate#(X) |
| add#(s(X), Y) | → | activate#(X) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__add(X1, X2)) | → | add#(X1, X2) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, n__dbl, first, cons, nil
Strategy
There are no SCCs!
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sqr#(s(X)) | → | sqr#(activate(X)) |
Rewrite Rules
| terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) | | sqr(0) | → | 0 |
| sqr(s(X)) | → | s(n__add(sqr(activate(X)), dbl(activate(X)))) | | dbl(0) | → | 0 |
| dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | | add(0, X) | → | X |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | first(0, X) | → | nil |
| first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) | | terms(X) | → | n__terms(X) |
| add(X1, X2) | → | n__add(X1, X2) | | s(X) | → | n__s(X) |
| dbl(X) | → | n__dbl(X) | | first(X1, X2) | → | n__first(X1, X2) |
| activate(n__terms(X)) | → | terms(X) | | activate(n__add(X1, X2)) | → | add(X1, X2) |
| activate(n__s(X)) | → | s(X) | | activate(n__dbl(X)) | → | dbl(X) |
| activate(n__first(X1, X2)) | → | first(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, dbl, recip, n__terms, add, activate, n__s, 0, s, n__first, n__add, first, n__dbl, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): x
- add(x,y): y + 2x
- cons(x,y): x
- dbl(x): 2x
- first(x,y): y + 1
- n__add(x,y): y + 2x
- n__dbl(x): 2x
- n__first(x,y): y + 1
- n__s(x): x + 1
- n__terms(x): 2
- nil: 1
- recip(x): 2
- s(x): x + 1
- sqr(x): 1
- sqr#(x): x + 1
- terms(x): 2
Improved Usable rules
| first(X1, X2) | → | n__first(X1, X2) | | terms(X) | → | n__terms(X) |
| activate(n__add(X1, X2)) | → | add(X1, X2) | | terms(N) | → | cons(recip(sqr(N)), n__terms(s(N))) |
| activate(n__s(X)) | → | s(X) | | dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) |
| add(0, X) | → | X | | first(0, X) | → | nil |
| add(X1, X2) | → | n__add(X1, X2) | | activate(n__terms(X)) | → | terms(X) |
| dbl(0) | → | 0 | | first(s(X), cons(Y, Z)) | → | cons(Y, n__first(activate(X), activate(Z))) |
| s(X) | → | n__s(X) | | activate(n__first(X1, X2)) | → | first(X1, X2) |
| activate(X) | → | X | | dbl(X) | → | n__dbl(X) |
| add(s(X), Y) | → | s(n__add(activate(X), Y)) | | activate(n__dbl(X)) | → | dbl(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sqr#(s(X)) | → | sqr#(activate(X)) |