TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60033 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (343ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (4141ms).
| | – Problem 3 was processed with processor DependencyGraph (68ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (1917ms).
| | | | – Problem 5 was processed with processor DependencyGraph (19ms).
| | | | | – Problem 6 remains open; application of the following processors failed [PolynomialLinearRange4iUR (647ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (10250ms), DependencyGraph (12ms), ReductionPairSAT (1914ms), DependencyGraph (10ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| activate#(n__oddNs) | → | oddNs# | | activate#(n__cons(X1, X2)) | → | activate#(X1) |
| activate#(n__incr(X)) | → | incr#(activate(X)) | | oddNs# | → | incr#(pairNs) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | activate#(X) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| zip#(cons(X, XS), cons(Y, YS)) | → | cons#(pair(X, Y), n__zip(activate(XS), activate(YS))) | | activate#(n__incr(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | tail#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | activate#(n__incr(X)) | → | incr#(activate(X)) |
| repItems#(cons(X, XS)) | → | activate#(XS) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| pairNs# | → | cons#(0, n__incr(n__oddNs)) | | activate#(n__take(X1, X2)) | → | activate#(X2) |
| activate#(n__oddNs) | → | oddNs# | | incr#(cons(X, XS)) | → | cons#(s(X), n__incr(activate(XS))) |
| oddNs# | → | incr#(pairNs) | | incr#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__zip(X1, X2)) | → | activate#(X2) | | take#(s(N), cons(X, XS)) | → | activate#(XS) |
| activate#(n__repItems(X)) | → | repItems#(activate(X)) | | activate#(n__repItems(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | activate#(n__zip(X1, X2)) | → | zip#(activate(X1), activate(X2)) |
| oddNs# | → | pairNs# | | activate#(n__zip(X1, X2)) | → | activate#(X1) |
| take#(s(N), cons(X, XS)) | → | cons#(X, n__take(N, activate(XS))) | | repItems#(cons(X, XS)) | → | cons#(X, n__cons(X, n__repItems(activate(XS)))) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons
Strategy
The following SCCs where found
| activate#(n__oddNs) → oddNs# | oddNs# → incr#(pairNs) |
| incr#(cons(X, XS)) → activate#(XS) | activate#(n__incr(X)) → activate#(X) |
| activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) | activate#(n__zip(X1, X2)) → activate#(X2) |
| activate#(n__repItems(X)) → repItems#(activate(X)) | take#(s(N), cons(X, XS)) → activate#(XS) |
| activate#(n__repItems(X)) → activate#(X) | zip#(cons(X, XS), cons(Y, YS)) → activate#(XS) |
| activate#(n__cons(X1, X2)) → activate#(X1) | activate#(n__incr(X)) → incr#(activate(X)) |
| activate#(n__zip(X1, X2)) → zip#(activate(X1), activate(X2)) | repItems#(cons(X, XS)) → activate#(XS) |
| activate#(n__take(X1, X2)) → activate#(X1) | zip#(cons(X, XS), cons(Y, YS)) → activate#(YS) |
| activate#(n__zip(X1, X2)) → activate#(X1) | activate#(n__take(X1, X2)) → activate#(X2) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__oddNs) | → | oddNs# | | oddNs# | → | incr#(pairNs) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | activate#(n__zip(X1, X2)) | → | activate#(X2) |
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | activate#(n__repItems(X)) | → | repItems#(activate(X)) |
| activate#(n__repItems(X)) | → | activate#(X) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | activate#(n__incr(X)) | → | incr#(activate(X)) |
| activate#(n__zip(X1, X2)) | → | zip#(activate(X1), activate(X2)) | | repItems#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| activate#(n__zip(X1, X2)) | → | activate#(X1) | | activate#(n__take(X1, X2)) | → | activate#(X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): x
- activate#(x): x
- cons(x,y): y + x
- incr(x): 2x
- incr#(x): 2x
- n__cons(x,y): y + x
- n__incr(x): 2x
- n__oddNs: 0
- n__repItems(x): 2x
- n__take(x,y): 2y + x
- n__zip(x,y): y + x + 2
- nil: 0
- oddNs: 0
- oddNs#: 0
- pair(x,y): y + x
- pairNs: 0
- repItems(x): 2x
- repItems#(x): x
- s(x): 2x
- tail(x): 0
- take(x,y): 2y + x
- take#(x,y): y
- zip(x,y): y + x + 2
- zip#(x,y): y + x
Improved Usable rules
| repItems(X) | → | n__repItems(X) | | zip(nil, XS) | → | nil |
| take(0, XS) | → | nil | | take(X1, X2) | → | n__take(X1, X2) |
| oddNs | → | n__oddNs | | zip(X, nil) | → | nil |
| activate(n__oddNs) | → | oddNs | | oddNs | → | incr(pairNs) |
| activate(n__repItems(X)) | → | repItems(activate(X)) | | cons(X1, X2) | → | n__cons(X1, X2) |
| activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) | | activate(n__incr(X)) | → | incr(activate(X)) |
| pairNs | → | cons(0, n__incr(n__oddNs)) | | activate(X) | → | X |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | incr(X) | → | n__incr(X) |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) |
| repItems(nil) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__zip(X1, X2)) | → | activate#(X2) | | activate#(n__zip(X1, X2)) | → | zip#(activate(X1), activate(X2)) |
| activate#(n__zip(X1, X2)) | → | activate#(X1) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__oddNs) | → | oddNs# | | oddNs# | → | incr#(pairNs) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | take#(s(N), cons(X, XS)) | → | activate#(XS) |
| activate#(n__repItems(X)) | → | repItems#(activate(X)) | | activate#(n__repItems(X)) | → | activate#(X) |
| zip#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | activate#(n__cons(X1, X2)) | → | activate#(X1) |
| activate#(n__incr(X)) | → | incr#(activate(X)) | | repItems#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | zip#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| activate#(n__take(X1, X2)) | → | activate#(X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
The following SCCs where found
| activate#(n__oddNs) → oddNs# | oddNs# → incr#(pairNs) |
| incr#(cons(X, XS)) → activate#(XS) | activate#(n__incr(X)) → activate#(X) |
| activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) | take#(s(N), cons(X, XS)) → activate#(XS) |
| activate#(n__repItems(X)) → repItems#(activate(X)) | activate#(n__repItems(X)) → activate#(X) |
| activate#(n__cons(X1, X2)) → activate#(X1) | activate#(n__incr(X)) → incr#(activate(X)) |
| repItems#(cons(X, XS)) → activate#(XS) | activate#(n__take(X1, X2)) → activate#(X1) |
| activate#(n__take(X1, X2)) → activate#(X2) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__oddNs) | → | oddNs# | | oddNs# | → | incr#(pairNs) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | activate#(n__repItems(X)) | → | repItems#(activate(X)) |
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | activate#(n__repItems(X)) | → | activate#(X) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | activate#(n__incr(X)) | → | incr#(activate(X)) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | repItems#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | activate#(X2) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): x
- activate#(x): x
- cons(x,y): y + 2x
- incr(x): 2x
- incr#(x): 2x
- n__cons(x,y): y + 2x
- n__incr(x): 2x
- n__oddNs: 0
- n__repItems(x): 2x + 2
- n__take(x,y): y + x + 2
- n__zip(x,y): 2
- nil: 0
- oddNs: 0
- oddNs#: 0
- pair(x,y): 0
- pairNs: 0
- repItems(x): 2x + 2
- repItems#(x): x + 2
- s(x): x
- tail(x): 0
- take(x,y): y + x + 2
- take#(x,y): y + x
- zip(x,y): 2
Improved Usable rules
| repItems(X) | → | n__repItems(X) | | zip(nil, XS) | → | nil |
| take(0, XS) | → | nil | | take(X1, X2) | → | n__take(X1, X2) |
| oddNs | → | n__oddNs | | zip(X, nil) | → | nil |
| activate(n__oddNs) | → | oddNs | | oddNs | → | incr(pairNs) |
| activate(n__repItems(X)) | → | repItems(activate(X)) | | cons(X1, X2) | → | n__cons(X1, X2) |
| activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) | | activate(n__incr(X)) | → | incr(activate(X)) |
| pairNs | → | cons(0, n__incr(n__oddNs)) | | activate(X) | → | X |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | incr(X) | → | n__incr(X) |
| take(s(N), cons(X, XS)) | → | cons(X, n__take(N, activate(XS))) | | zip(cons(X, XS), cons(Y, YS)) | → | cons(pair(X, Y), n__zip(activate(XS), activate(YS))) |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | | zip(X1, X2) | → | n__zip(X1, X2) |
| repItems(cons(X, XS)) | → | cons(X, n__cons(X, n__repItems(activate(XS)))) | | incr(cons(X, XS)) | → | cons(s(X), n__incr(activate(XS))) |
| repItems(nil) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | activate#(n__repItems(X)) | → | activate#(X) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | repItems#(cons(X, XS)) | → | activate#(XS) |
| activate#(n__take(X1, X2)) | → | activate#(X2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(s(N), cons(X, XS)) | → | activate#(XS) | | activate#(n__repItems(X)) | → | repItems#(activate(X)) |
| activate#(n__oddNs) | → | oddNs# | | activate#(n__cons(X1, X2)) | → | activate#(X1) |
| activate#(n__incr(X)) | → | incr#(activate(X)) | | oddNs# | → | incr#(pairNs) |
| incr#(cons(X, XS)) | → | activate#(XS) | | activate#(n__incr(X)) | → | activate#(X) |
Rewrite Rules
| pairNs | → | cons(0, n__incr(n__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) |
| oddNs | → | n__oddNs | | 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(activate(X)) |
| activate(n__oddNs) | → | oddNs | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(n__zip(X1, X2)) | → | zip(activate(X1), activate(X2)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__repItems(X)) | → | repItems(activate(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, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons
Strategy
The following SCCs where found
| activate#(n__oddNs) → oddNs# | activate#(n__cons(X1, X2)) → activate#(X1) |
| activate#(n__incr(X)) → incr#(activate(X)) | oddNs# → incr#(pairNs) |
| incr#(cons(X, XS)) → activate#(XS) | activate#(n__incr(X)) → activate#(X) |