The TRS could be proven non-terminating. The proof took 1055 ms.
The following reduction sequence is a witness for non-termination:
pairNs# →* pairNs#
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor Propagation (3ms).
| | – Problem 10 remains open; application of the following processors failed [BackwardsNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (3ms)].
| – Problem 3 was processed with processor PolynomialOrdering (0ms).
| | – Problem 4 was processed with processor DependencyGraph (0ms).
| | | – Problem 5 was processed with processor PolynomialOrdering (0ms).
| | | | – Problem 6 was processed with processor DependencyGraph (0ms).
| | | | | – Problem 7 was processed with processor PolynomialOrdering (0ms).
| | | | | | – Problem 8 was processed with processor DependencyGraph (0ms).
| | | | | | | – Problem 9 was processed with processor PolynomialOrdering (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| incr#(cons(X, XS)) | → | cons#(s(X), n__incr(activate(XS))) | | oddNs# | → | incr#(pairNs) |
| zip#(cons(X, XS), cons(Y, YS)) | → | cons#(pair(X, Y), n__zip(activate(XS), activate(YS))) | | incr#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__incr(X)) | → | incr#(X) | | pairNs# | → | cons#(0, n__incr(oddNs)) |
| tail#(cons(X, XS)) | → | activate#(XS) | | take#(s(N), cons(X, XS)) | → | activate#(XS) |
| activate#(n__repItems(X)) | → | repItems#(X) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| repItems#(cons(X, XS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| pairNs# | → | oddNs# | | oddNs# | → | pairNs# |
| activate#(n__take(X1, X2)) | → | take#(X1, X2) | | take#(s(N), cons(X, XS)) | → | cons#(X, n__take(N, activate(XS))) |
| activate#(n__cons(X1, X2)) | → | cons#(X1, X2) | | repItems#(cons(X, XS)) | → | cons#(X, n__cons(X, n__repItems(activate(XS)))) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| pairNs# → oddNs# | oddNs# → pairNs# |
| take#(s(N), cons(X, XS)) → activate#(XS) | activate#(n__repItems(X)) → repItems#(X) |
| zip#(cons(X, XS), cons(Y, YS)) → activate#(XS) | repItems#(cons(X, XS)) → activate#(XS) |
| zip#(cons(X, XS), cons(Y, YS)) → activate#(YS) | incr#(cons(X, XS)) → activate#(XS) |
| activate#(n__take(X1, X2)) → take#(X1, X2) | activate#(n__incr(X)) → incr#(X) |
| activate#(n__zip(X1, X2)) → zip#(X1, X2) |
Problem 2: Propagation
Dependency Pair Problem
Dependency Pairs
| pairNs# | → | oddNs# | | oddNs# | → | pairNs# |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons
Strategy
The dependency pairs pairNs
# → oddNs
# and oddNs
# → pairNs
# are consolidated into the rule pairNs
# → pairNs
# .
This is possible as
- all subterms of oddNs# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in oddNs#, but non-replacing in both pairNs# and pairNs#
The dependency pairs pairNs
# → oddNs
# and oddNs
# → pairNs
# are consolidated into the rule pairNs
# → pairNs
# .
This is possible as
- all subterms of oddNs# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in oddNs#, but non-replacing in both pairNs# and pairNs#
The dependency pairs oddNs
# → pairNs
# and pairNs
# → oddNs
# are consolidated into the rule oddNs
# → oddNs
# .
This is possible as
- all subterms of pairNs# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in pairNs#, but non-replacing in both oddNs# and oddNs#
The dependency pairs oddNs
# → pairNs
# and pairNs
# → oddNs
# are consolidated into the rule oddNs
# → oddNs
# .
This is possible as
- all subterms of pairNs# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in pairNs#, but non-replacing in both oddNs# and oddNs#
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| pairNs# → oddNs# | pairNs# → pairNs# |
| oddNs# → pairNs# | oddNs# → oddNs# |
Problem 3: PolynomialOrdering
Dependency Pair Problem
Dependency Pairs
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | activate#(n__repItems(X)) | → | repItems#(X) |
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | repItems#(cons(X, XS)) | → | activate#(XS) |
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) | | incr#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | take#(X1, X2) | | activate#(n__incr(X)) | → | incr#(X) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons
Strategy
Parameters
- Usable Rules: Improved
- Polynomial Degree: Linear
- Use negative constants: false
- Coefficient Range: 4
- Negative Constant Range: 0
Polynomial Interpretation
- 0: 0
- activate(x): 0
- activate#(x): 3x
- cons(x,y): 3y
- incr(x): 0
- incr#(x): x
- n__cons(x,y): 0
- n__incr(x): 3x
- n__repItems(x): 3x + 1
- n__take(x,y): 3y + 3x
- n__zip(x,y): y + 3x
- nil: 0
- oddNs: 0
- pair(x,y): 0
- pairNs: 0
- repItems(x): 0
- repItems#(x): 2x + 3
- s(x): 2x + 2
- tail(x): 0
- take(x,y): 0
- take#(x,y): 2y
- zip(x,y): 0
- zip#(x,y): 2y + x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| repItems#(cons(X, XS)) | → | activate#(XS) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| activate#(n__repItems(X)) | → | repItems#(X) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__take(X1, X2)) | → | take#(X1, X2) |
| activate#(n__incr(X)) | → | incr#(X) | | activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| take#(s(N), cons(X, XS)) → activate#(XS) | zip#(cons(X, XS), cons(Y, YS)) → activate#(XS) |
| zip#(cons(X, XS), cons(Y, YS)) → activate#(YS) | incr#(cons(X, XS)) → activate#(XS) |
| activate#(n__take(X1, X2)) → take#(X1, X2) | activate#(n__incr(X)) → incr#(X) |
| activate#(n__zip(X1, X2)) → zip#(X1, X2) |
Problem 5: PolynomialOrdering
Dependency Pair Problem
Dependency Pairs
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) | | incr#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | take#(X1, X2) | | activate#(n__incr(X)) | → | incr#(X) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
Parameters
- Usable Rules: Improved
- Polynomial Degree: Linear
- Use negative constants: false
- Coefficient Range: 4
- Negative Constant Range: 0
Polynomial Interpretation
- 0: 0
- activate(x): 0
- activate#(x): 2x
- cons(x,y): 2y + 3x
- incr(x): 0
- incr#(x): x
- n__cons(x,y): 0
- n__incr(x): 2x
- n__repItems(x): 0
- n__take(x,y): y + 2x
- n__zip(x,y): 2y + 2x
- nil: 0
- oddNs: 0
- pair(x,y): 0
- pairNs: 0
- repItems(x): 0
- s(x): 1
- tail(x): 0
- take(x,y): 0
- take#(x,y): 2y + x
- zip(x,y): 0
- zip#(x,y): 2y + 2x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| take#(s(N), cons(X, XS)) | → | activate#(XS) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__take(X1, X2)) | → | take#(X1, X2) |
| activate#(n__incr(X)) | → | incr#(X) | | activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| zip#(cons(X, XS), cons(Y, YS)) → activate#(XS) | zip#(cons(X, XS), cons(Y, YS)) → activate#(YS) |
| incr#(cons(X, XS)) → activate#(XS) | activate#(n__incr(X)) → incr#(X) |
| activate#(n__zip(X1, X2)) → zip#(X1, X2) |
Problem 7: PolynomialOrdering
Dependency Pair Problem
Dependency Pairs
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | incr#(X) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, nil, cons
Strategy
Parameters
- Usable Rules: Improved
- Polynomial Degree: Linear
- Use negative constants: false
- Coefficient Range: 4
- Negative Constant Range: 0
Polynomial Interpretation
- 0: 0
- activate(x): 0
- activate#(x): 2x
- cons(x,y): 2y
- incr(x): 0
- incr#(x): x + 2
- n__cons(x,y): 0
- n__incr(x): x + 1
- n__repItems(x): 0
- n__take(x,y): 0
- n__zip(x,y): y + x
- nil: 0
- oddNs: 0
- pair(x,y): 0
- pairNs: 0
- repItems(x): 0
- s(x): 0
- tail(x): 0
- take(x,y): 0
- zip(x,y): 0
- zip#(x,y): y + x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| incr#(cons(X, XS)) | → | activate#(XS) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| activate#(n__incr(X)) | → | incr#(X) | | activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| zip#(cons(X, XS), cons(Y, YS)) → activate#(XS) | zip#(cons(X, XS), cons(Y, YS)) → activate#(YS) |
| activate#(n__zip(X1, X2)) → zip#(X1, X2) |
Problem 9: PolynomialOrdering
Dependency Pair Problem
Dependency Pairs
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(oddNs)) | | oddNs | → | incr(pairNs) |
| incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) | | take(0, XS) | → | nil |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(nil, XS) | → | nil |
| zip(X, nil) | → | nil | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| tail(cons(X, XS)) | → | activate(XS) | | repItems(nil) | → | nil |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(X) | → | n__incr(X) |
| take(X1, X2) | → | n__take(X1, X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| cons(X1, X2) | → | n__cons(X1, X2) | | repItems(X) | → | n__repItems(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__take(X1, X2)) | → | take(X1, X2) |
| activate(n__zip(X1, X2)) | → | zip(X1, X2) | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(n__repItems(X)) | → | repItems(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
Parameters
- Usable Rules: Improved
- Polynomial Degree: Linear
- Use negative constants: false
- Coefficient Range: 4
- Negative Constant Range: 0
Polynomial Interpretation
- 0: 0
- activate(x): 0
- activate#(x): 2x + 1
- cons(x,y): 3y + 2x + 1
- incr(x): 0
- n__cons(x,y): 0
- n__incr(x): 0
- n__repItems(x): 0
- n__take(x,y): 0
- n__zip(x,y): 2y + x
- nil: 0
- oddNs: 0
- pair(x,y): 0
- pairNs: 0
- repItems(x): 0
- s(x): 0
- tail(x): 0
- take(x,y): 0
- zip(x,y): 0
- zip#(x,y): y + x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| activate#(n__zip(X1, X2)) | → | zip#(X1, X2) |