The TRS could be proven non-terminating. The proof took 371 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 (0ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 6 was processed with processor BackwardInstantiation (4ms).
| | | – Problem 8 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 10 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (2ms)].
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor BackwardInstantiation (2ms).
| | – Problem 7 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 9 was processed with processor BackwardInstantiation (2ms).
| | | | – Problem 11 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, nil)) | | prefix#(L) | → | prefix#(L) |
| app#(cons(X, XS), YS) | → | app#(XS, YS) | | from#(X) | → | from#(s(X)) |
| prefix#(L) | → | zWadr#(L, prefix(L)) | | zWadr#(cons(X, XS), cons(Y, YS)) | → | zWadr#(XS, YS) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| app#(cons(X, XS), YS) → app#(XS, YS) |
| zWadr#(cons(X, XS), cons(Y, YS)) → zWadr#(XS, YS) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, 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, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, 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 8: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| prefix#(__L) | → | prefix#(__L) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, 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 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| zWadr#(cons(X, XS), cons(Y, YS)) | → | zWadr#(XS, YS) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| zWadr#(cons(X, XS), cons(Y, YS)) | → | zWadr#(XS, YS) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(cons(X, XS), YS) | → | app#(XS, YS) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(cons(X, XS), YS) | → | app#(XS, YS) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule from
#(
X) → from
#(s(
X)) on dependency pair chains it holds that:
- from#(X) matches r,
- all variables of from#(X) are embedded in constructor contexts, i.e., each subterm of from#(X), containing a variable is rooted by a constructor symbol.
Thus, from
#(
X) → from
#(s(
X)) is replaced by instances determined through the above matching. These instances are:
| from#(s(_X)) → from#(s(s(_X))) |
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| from#(s(_X)) | → | from#(s(s(_X))) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule from
#(s(
_X)) → from
#(s(s(
_X))) on dependency pair chains it holds that:
- from#(s(_X)) matches r,
- all variables of from#(s(_X)) are embedded in constructor contexts, i.e., each subterm of from#(s(_X)), containing a variable is rooted by a constructor symbol.
Thus, from
#(s(
_X)) → from
#(s(s(
_X))) is replaced by instances determined through the above matching. These instances are:
| from#(s(s(__X))) → from#(s(s(s(__X)))) |
Problem 9: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| from#(s(s(__X))) | → | from#(s(s(s(__X)))) |
Rewrite Rules
| app(nil, YS) | → | YS | | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) |
| from(X) | → | cons(X, from(s(X))) | | zWadr(nil, YS) | → | nil |
| zWadr(XS, nil) | → | nil | | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Original Signature
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule from
#(s(s(
__X))) → from
#(s(s(s(
__X)))) on dependency pair chains it holds that:
- from#(s(s(__X))) matches r,
- all variables of from#(s(s(__X))) are embedded in constructor contexts, i.e., each subterm of from#(s(s(__X))), containing a variable is rooted by a constructor symbol.
Thus, from
#(s(s(
__X))) → from
#(s(s(s(
__X)))) is replaced by instances determined through the above matching. These instances are:
| from#(s(s(s(___X)))) → from#(s(s(s(s(___X))))) |