NO
The TRS could be proven non-terminating. The proof took 665 ms.
The following reduction sequence is a witness for non-termination:
prefix#(___L) →* prefix#(___L)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (64ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (214ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (97ms).
| | | – Problem 5 was processed with processor DependencyGraph (5ms).
| – Problem 3 was processed with processor BackwardInstantiation (1ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (2ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| prefix#(L) | → | nil# | | activate#(n__nil) | → | nil# |
| activate#(n__zWadr(X1, X2)) | → | zWadr#(X1, X2) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| app#(cons(X, XS), YS) | → | activate#(XS) | | zWadr#(XS, nil) | → | nil# |
| zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | prefix#(L) | → | prefix#(L) |
| zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, n__nil)) | | activate#(n__from(X)) | → | from#(X) |
| zWadr#(nil, YS) | → | nil# | | activate#(n__app(X1, X2)) | → | app#(X1, X2) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons
Strategy
The following SCCs where found
| activate#(n__zWadr(X1, X2)) → zWadr#(X1, X2) | zWadr#(cons(X, XS), cons(Y, YS)) → activate#(YS) |
| app#(cons(X, XS), YS) → activate#(XS) | zWadr#(cons(X, XS), cons(Y, YS)) → activate#(XS) |
| zWadr#(cons(X, XS), cons(Y, YS)) → app#(Y, cons(X, n__nil)) | activate#(n__app(X1, X2)) → app#(X1, X2) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__zWadr(X1, X2)) | → | zWadr#(X1, X2) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| app#(cons(X, XS), YS) | → | activate#(XS) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, n__nil)) | | activate#(n__app(X1, X2)) | → | app#(X1, X2) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons
Strategy
Polynomial Interpretation
- activate(x): 0
- activate#(x): x
- app(x,y): 0
- app#(x,y): 2y + 2x
- cons(x,y): y + x
- from(x): 0
- n__app(x,y): 2y + 2x + 1
- n__from(x): 0
- n__nil: 0
- n__zWadr(x,y): 2y + 2x
- nil: 0
- prefix(x): 0
- s(x): 0
- zWadr(x,y): 0
- zWadr#(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:
| activate#(n__app(X1, X2)) | → | app#(X1, X2) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__zWadr(X1, X2)) | → | zWadr#(X1, X2) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) |
| app#(cons(X, XS), YS) | → | activate#(XS) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) |
| zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, n__nil)) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, n__from, s, n__zWadr, prefix, n__app, n__nil, from, cons, nil
Strategy
Polynomial Interpretation
- activate(x): 0
- activate#(x): x + 1
- app(x,y): 0
- app#(x,y): y + x + 1
- cons(x,y): 2y + x
- from(x): 0
- n__app(x,y): 0
- n__from(x): 0
- n__nil: 0
- n__zWadr(x,y): y + x + 1
- nil: 0
- prefix(x): 0
- s(x): 0
- zWadr(x,y): 0
- zWadr#(x,y): y + x + 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__zWadr(X1, X2)) | → | zWadr#(X1, X2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(YS) | | app#(cons(X, XS), YS) | → | activate#(XS) |
| zWadr#(cons(X, XS), cons(Y, YS)) | → | activate#(XS) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, n__nil)) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons
Strategy
There are no SCCs!
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule prefix
#(
L) → prefix
#(
L) on dependency pair chains it holds that:
- prefix#(L) matches r,
- all variables of prefix#(L) are embedded in constructor contexts, i.e., each subterm of prefix#(L), containing a variable is rooted by a constructor symbol.
Thus, prefix
#(
L) → prefix
#(
L) is replaced by instances determined through the above matching. These instances are:
| prefix#(_L) → prefix#(_L) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| prefix#(_L) | → | prefix#(_L) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, n__from, s, n__zWadr, prefix, n__app, n__nil, from, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule prefix
#(
_L) → prefix
#(
_L) on dependency pair chains it holds that:
- prefix#(_L) matches r,
- all variables of prefix#(_L) are embedded in constructor contexts, i.e., each subterm of prefix#(_L), containing a variable is rooted by a constructor symbol.
Thus, prefix
#(
_L) → prefix
#(
_L) is replaced by instances determined through the above matching. These instances are:
| prefix#(__L) → prefix#(__L) |
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| prefix#(__L) | → | prefix#(__L) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, n__app(activate(XS), YS)) |
| from(X) | → | cons(X, n__from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS))) |
| prefix(L) | → | cons(nil, n__zWadr(L, prefix(L))) | | app(X1, X2) | → | n__app(X1, X2) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| zWadr(X1, X2) | → | n__zWadr(X1, X2) | | activate(n__app(X1, X2)) | → | app(X1, X2) |
| activate(n__from(X)) | → | from(X) | | activate(n__nil) | → | nil |
| activate(n__zWadr(X1, X2)) | → | zWadr(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule prefix
#(
__L) → prefix
#(
__L) on dependency pair chains it holds that:
- prefix#(__L) matches r,
- all variables of prefix#(__L) are embedded in constructor contexts, i.e., each subterm of prefix#(__L), containing a variable is rooted by a constructor symbol.
Thus, prefix
#(
__L) → prefix
#(
__L) is replaced by instances determined through the above matching. These instances are:
| prefix#(___L) → prefix#(___L) |