YES
The TRS could be proven terminating. The proof took 3277 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (219ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (2018ms).
| | – Problem 3 was processed with processor DependencyGraph (10ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (684ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (23ms).
| | | | | – Problem 6 was processed with processor PolynomialLinearRange4iUR (22ms).
| | | | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (11ms).
| | | | | | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (8ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__terms#(N) | → | mark#(N) | | mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(dbl(X)) | → | a__dbl#(mark(X)) | | a__add#(0, X) | → | mark#(X) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(terms(X)) | → | mark#(X) |
| mark#(recip(X)) | → | mark#(X) | | mark#(sqr(X)) | → | mark#(X) |
| a__first#(s(X), cons(Y, Z)) | → | mark#(Y) | | mark#(sqr(X)) | → | a__sqr#(mark(X)) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(first(X1, X2)) | → | mark#(X1) |
| a__terms#(N) | → | a__sqr#(mark(N)) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil
Strategy
The following SCCs where found
| mark#(terms(X)) → a__terms#(mark(X)) | mark#(first(X1, X2)) → mark#(X2) |
| a__terms#(N) → mark#(N) | mark#(first(X1, X2)) → a__first#(mark(X1), mark(X2)) |
| mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2)) | mark#(cons(X1, X2)) → mark#(X1) |
| a__add#(0, X) → mark#(X) | mark#(dbl(X)) → mark#(X) |
| mark#(terms(X)) → mark#(X) | mark#(sqr(X)) → mark#(X) |
| mark#(recip(X)) → mark#(X) | a__first#(s(X), cons(Y, Z)) → mark#(Y) |
| mark#(first(X1, X2)) → mark#(X1) | mark#(add(X1, X2)) → mark#(X2) |
| mark#(add(X1, X2)) → mark#(X1) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__add#(0, X) | → | mark#(X) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | mark#(recip(X)) | → | mark#(X) |
| mark#(sqr(X)) | → | mark#(X) | | a__first#(s(X), cons(Y, Z)) | → | mark#(Y) |
| mark#(first(X1, X2)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__add(x,y): y + 2x
- a__add#(x,y): y
- a__dbl(x): x + 2
- a__first(x,y): 3y + x + 2
- a__first#(x,y): 2y + x
- a__sqr(x): x
- a__terms(x): x + 2
- a__terms#(x): x
- add(x,y): y + 2x
- cons(x,y): x
- dbl(x): x + 2
- first(x,y): 3y + x + 2
- mark(x): x
- mark#(x): x
- nil: 1
- recip(x): x
- s(x): 1
- sqr(x): x
- terms(x): x + 2
Improved Usable rules
| a__terms(X) | → | terms(X) | | a__first(X1, X2) | → | first(X1, X2) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(s(X)) | → | s(X) |
| mark(terms(X)) | → | a__terms(mark(X)) | | mark(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) |
| a__first(0, X) | → | nil | | a__dbl(0) | → | 0 |
| a__sqr(0) | → | 0 | | a__add(X1, X2) | → | add(X1, X2) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | a__add(s(X), Y) | → | s(add(X, Y)) |
| a__sqr(X) | → | sqr(X) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(nil) | → | nil | | a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) |
| mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) | | a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) |
| a__dbl(X) | → | dbl(X) | | a__add(0, X) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(terms(X)) | → | a__terms#(mark(X)) |
| mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(terms(X)) | → | mark#(X) | | a__first#(s(X), cons(Y, Z)) | → | mark#(Y) |
| mark#(first(X1, X2)) | → | mark#(X1) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(sqr(X)) | → | mark#(X) | | mark#(recip(X)) | → | mark#(X) |
| a__terms#(N) | → | mark#(N) | | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(add(X1, X2)) | → | mark#(X1) | | a__add#(0, X) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
The following SCCs where found
| mark#(sqr(X)) → mark#(X) | mark#(recip(X)) → mark#(X) |
| mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2)) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(add(X1, X2)) → mark#(X2) | mark#(add(X1, X2)) → mark#(X1) |
| a__add#(0, X) → mark#(X) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(sqr(X)) | → | mark#(X) | | mark#(recip(X)) | → | mark#(X) |
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(add(X1, X2)) | → | mark#(X1) |
| a__add#(0, X) | → | mark#(X) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Polynomial Interpretation
- 0: 1
- a__add(x,y): y + 2x
- a__add#(x,y): y + 2x
- a__dbl(x): 2
- a__first(x,y): y
- a__sqr(x): x
- a__terms(x): 2x
- add(x,y): y + 2x
- cons(x,y): y + x
- dbl(x): 2
- first(x,y): y
- mark(x): x
- mark#(x): x + 1
- nil: 0
- recip(x): 2x
- s(x): 0
- sqr(x): x
- terms(x): 2x
Improved Usable rules
| a__terms(X) | → | terms(X) | | a__first(X1, X2) | → | first(X1, X2) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(s(X)) | → | s(X) |
| mark(terms(X)) | → | a__terms(mark(X)) | | mark(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) |
| a__first(0, X) | → | nil | | a__dbl(0) | → | 0 |
| a__sqr(0) | → | 0 | | a__add(X1, X2) | → | add(X1, X2) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | a__add(s(X), Y) | → | s(add(X, Y)) |
| a__sqr(X) | → | sqr(X) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(nil) | → | nil | | a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) |
| mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) | | a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) |
| a__dbl(X) | → | dbl(X) | | a__add(0, X) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | | a__add#(0, X) | → | mark#(X) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(sqr(X)) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X2) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__add(x,y): 0
- a__dbl(x): 0
- a__first(x,y): 0
- a__sqr(x): 0
- a__terms(x): 0
- add(x,y): y + x
- cons(x,y): y + 3x
- dbl(x): 0
- first(x,y): 0
- mark(x): 0
- mark#(x): 3x
- nil: 0
- recip(x): x
- s(x): 0
- sqr(x): x + 1
- 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:
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- a__add(x,y): 0
- a__dbl(x): 0
- a__first(x,y): 0
- a__sqr(x): 0
- a__terms(x): 0
- add(x,y): y + 2x + 1
- cons(x,y): 2x
- dbl(x): 0
- first(x,y): 0
- mark(x): 0
- mark#(x): 2x
- nil: 0
- recip(x): 3x
- s(x): 0
- 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:
| mark#(add(X1, X2)) | → | mark#(X2) | | mark#(add(X1, X2)) | → | mark#(X1) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(recip(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__add(x,y): 0
- a__dbl(x): 0
- a__first(x,y): 0
- a__sqr(x): 0
- a__terms(x): 0
- add(x,y): 0
- cons(x,y): 2y + x
- dbl(x): 0
- first(x,y): 0
- mark(x): 0
- mark#(x): 2x
- nil: 0
- recip(x): 2x + 1
- s(x): 0
- 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:
| mark#(recip(X)) | → | mark#(X) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(cons(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__terms(N) | → | cons(recip(a__sqr(mark(N))), terms(s(N))) | | a__sqr(0) | → | 0 |
| a__sqr(s(X)) | → | s(add(sqr(X), dbl(X))) | | a__dbl(0) | → | 0 |
| a__dbl(s(X)) | → | s(s(dbl(X))) | | a__add(0, X) | → | mark(X) |
| a__add(s(X), Y) | → | s(add(X, Y)) | | a__first(0, X) | → | nil |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | | mark(terms(X)) | → | a__terms(mark(X)) |
| mark(sqr(X)) | → | a__sqr(mark(X)) | | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) |
| mark(dbl(X)) | → | a__dbl(mark(X)) | | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(recip(X)) | → | recip(mark(X)) |
| mark(s(X)) | → | s(X) | | mark(0) | → | 0 |
| mark(nil) | → | nil | | a__terms(X) | → | terms(X) |
| a__sqr(X) | → | sqr(X) | | a__add(X1, X2) | → | add(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__first(X1, X2) | → | first(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- a__add(x,y): 0
- a__dbl(x): 0
- a__first(x,y): 0
- a__sqr(x): 0
- a__terms(x): 0
- add(x,y): 0
- cons(x,y): x + 2
- dbl(x): 0
- first(x,y): 0
- mark(x): 0
- mark#(x): x + 1
- nil: 0
- recip(x): 0
- s(x): 0
- 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:
| mark#(cons(X1, X2)) | → | mark#(X1) |