TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (399ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (6986ms).
| | – Problem 3 was processed with processor DependencyGraph (179ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (4190ms).
| | | | – Problem 5 was processed with processor DependencyGraph (121ms).
| | | | | – Problem 6 was processed with processor PolynomialLinearRange4iUR (2995ms).
| | | | | | – Problem 7 was processed with processor DependencyGraph (95ms).
| | | | | | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (1831ms).
| | | | | | | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (3304ms).
| | | | | | | | | – Problem 10 was processed with processor DependencyGraph (28ms).
| | | | | | | | | | – Problem 11 was processed with processor PolynomialLinearRange4iUR (524ms).
| | | | | | | | | | | – Problem 12 remains open; application of the following processors failed [DependencyGraph (9ms), PolynomialLinearRange4iUR (835ms), DependencyGraph (32ms), PolynomialLinearRange8NegiUR (23286ms), DependencyGraph (8ms), ReductionPairSAT (2836ms), DependencyGraph (30ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 12
Dependency Pairs
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(incr(X)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(zip(X1, X2)) | → | mark#(X2) | | mark#(take(X1, X2)) | → | mark#(X1) |
| a__tail#(cons(X, XS)) | → | mark#(XS) | | mark#(incr(X)) | → | a__incr#(mark(X)) |
| mark#(pair(X1, X2)) | → | mark#(X2) | | mark#(zip(X1, X2)) | → | mark#(X1) |
| a__oddNs# | → | a__pairNs# | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(tail(X)) | → | a__tail#(mark(X)) |
| mark#(repItems(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) | | a__oddNs# | → | a__incr#(a__pairNs) |
| mark#(incr(X)) | → | mark#(X) | | a__take#(s(N), cons(X, XS)) | → | mark#(X) |
| mark#(pairNs) | → | a__pairNs# | | mark#(pair(X1, X2)) | → | mark#(X1) |
| mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | | mark#(tail(X)) | → | mark#(X) |
| mark#(repItems(X)) | → | a__repItems#(mark(X)) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | mark#(take(X1, X2)) | → | mark#(X2) |
| mark#(oddNs) | → | a__oddNs# | | a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, take, repItems, incr, a__pairNs, oddNs, nil, cons
Strategy
The following SCCs where found
| mark#(repItems(X)) → mark#(X) | mark#(zip(X1, X2)) → mark#(X2) |
| a__tail#(cons(X, XS)) → mark#(XS) | mark#(take(X1, X2)) → mark#(X1) |
| mark#(incr(X)) → a__incr#(mark(X)) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(pair(X1, X2)) → mark#(X2) | mark#(zip(X1, X2)) → a__zip#(mark(X1), mark(X2)) |
| mark#(zip(X1, X2)) → mark#(X1) | a__oddNs# → a__incr#(a__pairNs) |
| mark#(incr(X)) → mark#(X) | a__take#(s(N), cons(X, XS)) → mark#(X) |
| mark#(pair(X1, X2)) → mark#(X1) | mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2)) |
| mark#(tail(X)) → mark#(X) | mark#(repItems(X)) → a__repItems#(mark(X)) |
| a__zip#(cons(X, XS), cons(Y, YS)) → mark#(X) | mark#(take(X1, X2)) → mark#(X2) |
| a__zip#(cons(X, XS), cons(Y, YS)) → mark#(Y) | a__incr#(cons(X, XS)) → mark#(X) |
| mark#(s(X)) → mark#(X) | mark#(tail(X)) → a__tail#(mark(X)) |
| mark#(oddNs) → a__oddNs# | a__repItems#(cons(X, XS)) → mark#(X) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| mark#(take(X1, X2)) | → | mark#(X1) | | a__tail#(cons(X, XS)) | → | mark#(XS) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) | | a__oddNs# | → | a__incr#(a__pairNs) |
| mark#(incr(X)) | → | mark#(X) | | a__take#(s(N), cons(X, XS)) | → | mark#(X) |
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) |
| mark#(tail(X)) | → | mark#(X) | | mark#(repItems(X)) | → | a__repItems#(mark(X)) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X2) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(oddNs) | → | a__oddNs# | | mark#(tail(X)) | → | a__tail#(mark(X)) |
| mark#(s(X)) | → | mark#(X) | | a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, take, repItems, incr, a__pairNs, oddNs, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): 3x
- a__incr#(x): x
- a__oddNs: 0
- a__oddNs#: 0
- a__pairNs: 0
- a__repItems(x): 3x
- a__repItems#(x): x
- a__tail(x): 3x
- a__tail#(x): x
- a__take(x,y): 2y + 2x + 2
- a__take#(x,y): y
- a__zip(x,y): 2y + 2x
- a__zip#(x,y): y + x
- cons(x,y): y + x
- incr(x): 3x
- mark(x): 2x
- mark#(x): x
- nil: 1
- oddNs: 0
- pair(x,y): y + x
- pairNs: 0
- repItems(x): 3x
- s(x): x
- tail(x): 3x
- take(x,y): 2y + 2x + 1
- zip(x,y): 2y + 2x
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(take(X1, X2)) | → | mark#(X1) | | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) |
| mark#(take(X1, X2)) | → | mark#(X2) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| a__tail#(cons(X, XS)) | → | mark#(XS) | | mark#(incr(X)) | → | a__incr#(mark(X)) |
| mark#(pair(X1, X2)) | → | mark#(X2) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| a__oddNs# | → | a__incr#(a__pairNs) | | mark#(incr(X)) | → | mark#(X) |
| a__take#(s(N), cons(X, XS)) | → | mark#(X) | | mark#(pair(X1, X2)) | → | mark#(X1) |
| mark#(repItems(X)) | → | a__repItems#(mark(X)) | | mark#(tail(X)) | → | mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(tail(X)) | → | a__tail#(mark(X)) | | mark#(oddNs) | → | a__oddNs# |
| a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
The following SCCs where found
| mark#(repItems(X)) → mark#(X) | mark#(zip(X1, X2)) → mark#(X2) |
| a__tail#(cons(X, XS)) → mark#(XS) | mark#(incr(X)) → a__incr#(mark(X)) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(pair(X1, X2)) → mark#(X2) |
| mark#(zip(X1, X2)) → a__zip#(mark(X1), mark(X2)) | mark#(zip(X1, X2)) → mark#(X1) |
| a__oddNs# → a__incr#(a__pairNs) | mark#(incr(X)) → mark#(X) |
| mark#(pair(X1, X2)) → mark#(X1) | mark#(tail(X)) → mark#(X) |
| mark#(repItems(X)) → a__repItems#(mark(X)) | a__zip#(cons(X, XS), cons(Y, YS)) → mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) → mark#(Y) | a__incr#(cons(X, XS)) → mark#(X) |
| mark#(s(X)) → mark#(X) | mark#(tail(X)) → a__tail#(mark(X)) |
| mark#(oddNs) → a__oddNs# | a__repItems#(cons(X, XS)) → mark#(X) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| a__tail#(cons(X, XS)) | → | mark#(XS) | | mark#(incr(X)) | → | a__incr#(mark(X)) |
| mark#(pair(X1, X2)) | → | mark#(X2) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| a__oddNs# | → | a__incr#(a__pairNs) | | mark#(incr(X)) | → | mark#(X) |
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(repItems(X)) | → | a__repItems#(mark(X)) |
| mark#(tail(X)) | → | mark#(X) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(tail(X)) | → | a__tail#(mark(X)) |
| mark#(oddNs) | → | a__oddNs# | | a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): 2x
- a__incr#(x): 2x
- a__oddNs: 0
- a__oddNs#: 0
- a__pairNs: 0
- a__repItems(x): 2x
- a__repItems#(x): 2x
- a__tail(x): 3x + 1
- a__tail#(x): 2x + 1
- a__take(x,y): y + x
- a__zip(x,y): 2y + 2x
- a__zip#(x,y): 2y + 2x
- cons(x,y): y + 2x
- incr(x): 2x
- mark(x): x
- mark#(x): x
- nil: 0
- oddNs: 0
- pair(x,y): y + x
- pairNs: 0
- repItems(x): 2x
- s(x): x
- tail(x): 3x + 1
- take(x,y): y + x
- zip(x,y): 2y + 2x
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a__tail#(cons(X, XS)) | → | mark#(XS) | | mark#(tail(X)) | → | mark#(X) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) | | a__oddNs# | → | a__incr#(a__pairNs) |
| mark#(incr(X)) | → | mark#(X) | | mark#(pair(X1, X2)) | → | mark#(X1) |
| mark#(repItems(X)) | → | a__repItems#(mark(X)) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(oddNs) | → | a__oddNs# | | mark#(tail(X)) | → | a__tail#(mark(X)) |
| mark#(s(X)) | → | mark#(X) | | a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, take, repItems, incr, a__pairNs, oddNs, nil, cons
Strategy
The following SCCs where found
| mark#(repItems(X)) → mark#(X) | mark#(zip(X1, X2)) → mark#(X2) |
| mark#(incr(X)) → a__incr#(mark(X)) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(pair(X1, X2)) → mark#(X2) | mark#(zip(X1, X2)) → mark#(X1) |
| mark#(zip(X1, X2)) → a__zip#(mark(X1), mark(X2)) | a__oddNs# → a__incr#(a__pairNs) |
| mark#(incr(X)) → mark#(X) | mark#(pair(X1, X2)) → mark#(X1) |
| mark#(repItems(X)) → a__repItems#(mark(X)) | a__zip#(cons(X, XS), cons(Y, YS)) → mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) → mark#(Y) | a__incr#(cons(X, XS)) → mark#(X) |
| mark#(s(X)) → mark#(X) | mark#(oddNs) → a__oddNs# |
| a__repItems#(cons(X, XS)) → mark#(X) |
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| mark#(zip(X1, X2)) | → | mark#(X1) | | a__oddNs# | → | a__incr#(a__pairNs) |
| mark#(incr(X)) | → | mark#(X) | | mark#(pair(X1, X2)) | → | mark#(X1) |
| mark#(repItems(X)) | → | a__repItems#(mark(X)) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(oddNs) | → | a__oddNs# |
| a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, take, repItems, incr, a__pairNs, oddNs, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): x
- a__incr#(x): x
- a__oddNs: 1
- a__oddNs#: 2
- a__pairNs: 1
- a__repItems(x): 2x
- a__repItems#(x): 2x
- a__tail(x): x
- a__take(x,y): y + 2
- a__zip(x,y): 2y + 2x
- a__zip#(x,y): y + 2x
- cons(x,y): y + 2x
- incr(x): x
- mark(x): x
- mark#(x): 2x
- nil: 0
- oddNs: 1
- pair(x,y): y + x
- pairNs: 1
- repItems(x): 2x
- s(x): x
- tail(x): x
- take(x,y): y + 2
- zip(x,y): 2y + 2x
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a__oddNs# | → | a__incr#(a__pairNs) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| mark#(zip(X1, X2)) | → | mark#(X1) | | mark#(incr(X)) | → | mark#(X) |
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(repItems(X)) | → | a__repItems#(mark(X)) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(oddNs) | → | a__oddNs# |
| mark#(s(X)) | → | mark#(X) | | a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
The following SCCs where found
| mark#(repItems(X)) → mark#(X) | mark#(zip(X1, X2)) → mark#(X2) |
| mark#(incr(X)) → a__incr#(mark(X)) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(pair(X1, X2)) → mark#(X2) | mark#(zip(X1, X2)) → mark#(X1) |
| mark#(zip(X1, X2)) → a__zip#(mark(X1), mark(X2)) | mark#(incr(X)) → mark#(X) |
| mark#(pair(X1, X2)) → mark#(X1) | mark#(repItems(X)) → a__repItems#(mark(X)) |
| a__zip#(cons(X, XS), cons(Y, YS)) → mark#(X) | a__zip#(cons(X, XS), cons(Y, YS)) → mark#(Y) |
| a__incr#(cons(X, XS)) → mark#(X) | mark#(s(X)) → mark#(X) |
| a__repItems#(cons(X, XS)) → mark#(X) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(repItems(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X2) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| mark#(zip(X1, X2)) | → | mark#(X1) | | mark#(incr(X)) | → | mark#(X) |
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(repItems(X)) | → | a__repItems#(mark(X)) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| a__repItems#(cons(X, XS)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): 3x
- a__incr#(x): 2x
- a__oddNs: 0
- a__pairNs: 0
- a__repItems(x): 3x + 2
- a__repItems#(x): 3x + 1
- a__tail(x): 2x
- a__take(x,y): 3y + 2
- a__zip(x,y): 3y + 2x
- a__zip#(x,y): 2y + x
- cons(x,y): y + 2x
- incr(x): 3x
- mark(x): 2x
- mark#(x): 2x
- nil: 0
- oddNs: 0
- pair(x,y): y + x
- pairNs: 0
- repItems(x): 3x + 1
- s(x): x
- tail(x): 2x
- take(x,y): 3y + 1
- zip(x,y): 3y + 2x
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(repItems(X)) | → | mark#(X) | | mark#(repItems(X)) | → | a__repItems#(mark(X)) |
| a__repItems#(cons(X, XS)) | → | mark#(X) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(zip(X1, X2)) | → | mark#(X2) | | mark#(pair(X1, X2)) | → | mark#(X1) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | | a__incr#(cons(X, XS)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(zip(X1, X2)) | → | mark#(X1) |
| mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) | | mark#(incr(X)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, take, repItems, incr, a__pairNs, oddNs, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): 2x
- a__incr#(x): 2x
- a__oddNs: 0
- a__pairNs: 0
- a__repItems(x): 3x
- a__tail(x): 2x
- a__take(x,y): 2y
- a__zip(x,y): 2y + 2x + 2
- a__zip#(x,y): 2y + 2x
- cons(x,y): y + x
- incr(x): 2x
- mark(x): 2x
- mark#(x): 2x
- nil: 0
- oddNs: 0
- pair(x,y): y + x
- pairNs: 0
- repItems(x): 3x
- s(x): x
- tail(x): 2x
- take(x,y): 2y
- zip(x,y): 2y + 2x + 1
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(zip(X1, X2)) | → | mark#(X2) | | mark#(zip(X1, X2)) | → | a__zip#(mark(X1), mark(X2)) |
| mark#(zip(X1, X2)) | → | mark#(X1) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(incr(X)) | → | a__incr#(mark(X)) |
| mark#(pair(X1, X2)) | → | mark#(X2) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | | a__zip#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(incr(X)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
The following SCCs where found
| mark#(pair(X1, X2)) → mark#(X1) | mark#(incr(X)) → a__incr#(mark(X)) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(pair(X1, X2)) → mark#(X2) |
| a__incr#(cons(X, XS)) → mark#(X) | mark#(s(X)) → mark#(X) |
| mark#(incr(X)) → mark#(X) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(incr(X)) | → | a__incr#(mark(X)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(pair(X1, X2)) | → | mark#(X2) |
| a__incr#(cons(X, XS)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(incr(X)) | → | mark#(X) |
Rewrite Rules
| a__pairNs | → | cons(0, incr(oddNs)) | | a__oddNs | → | a__incr(a__pairNs) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__take(0, XS) | → | nil |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | | a__zip(nil, XS) | → | nil |
| a__zip(X, nil) | → | nil | | a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) |
| a__tail(cons(X, XS)) | → | mark(XS) | | a__repItems(nil) | → | nil |
| a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) | | mark(pairNs) | → | a__pairNs |
| mark(incr(X)) | → | a__incr(mark(X)) | | mark(oddNs) | → | a__oddNs |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(repItems(X)) | → | a__repItems(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(s(X)) | → | s(mark(X)) | | mark(nil) | → | nil |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | | a__pairNs | → | pairNs |
| a__incr(X) | → | incr(X) | | a__oddNs | → | oddNs |
| a__take(X1, X2) | → | take(X1, X2) | | a__zip(X1, X2) | → | zip(X1, X2) |
| a__tail(X) | → | tail(X) | | a__repItems(X) | → | repItems(X) |
Original Signature
Termination of terms over the following signature is verified: zip, a__zip, a__take, pair, a__oddNs, mark, tail, a__tail, 0, pairNs, a__incr, s, a__repItems, repItems, take, incr, oddNs, a__pairNs, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- a__incr(x): 3x
- a__incr#(x): x
- a__oddNs: 0
- a__pairNs: 0
- a__repItems(x): 3x + 2
- a__tail(x): 2x
- a__take(x,y): 2y + 2x
- a__zip(x,y): 2y + 2x + 2
- cons(x,y): y + x
- incr(x): 3x
- mark(x): 2x
- mark#(x): x
- nil: 0
- oddNs: 0
- pair(x,y): y + x + 1
- pairNs: 0
- repItems(x): 3x + 1
- s(x): x
- tail(x): 2x
- take(x,y): 2y + 2x
- zip(x,y): 2y + 2x + 1
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) |
| mark(zip(X1, X2)) | → | a__zip(mark(X1), mark(X2)) | | mark(oddNs) | → | a__oddNs |
| a__zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(mark(X), mark(Y)), zip(XS, YS)) | | a__oddNs | → | oddNs |
| mark(repItems(X)) | → | a__repItems(mark(X)) | | a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) |
| mark(nil) | → | nil | | a__take(X1, X2) | → | take(X1, X2) |
| a__incr(cons(X, XS)) | → | cons(s(mark(X)), incr(XS)) | | a__zip(X, nil) | → | nil |
| a__take(0, XS) | → | nil | | mark(0) | → | 0 |
| a__oddNs | → | a__incr(a__pairNs) | | a__tail(X) | → | tail(X) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(pairNs) | → | a__pairNs |
| a__zip(X1, X2) | → | zip(X1, X2) | | a__tail(cons(X, XS)) | → | mark(XS) |
| mark(incr(X)) | → | a__incr(mark(X)) | | a__repItems(cons(X, XS)) | → | cons(mark(X), cons(X, repItems(XS))) |
| mark(s(X)) | → | s(mark(X)) | | a__incr(X) | → | incr(X) |
| a__zip(nil, XS) | → | nil | | a__repItems(nil) | → | nil |
| a__pairNs | → | cons(0, incr(oddNs)) | | a__repItems(X) | → | repItems(X) |
| a__pairNs | → | pairNs | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(pair(X1, X2)) | → | mark#(X1) | | mark#(pair(X1, X2)) | → | mark#(X2) |