NO
The TRS could be proven non-terminating. The proof took 5663 ms.
The following reduction sequence is a witness for non-termination:
*#(___X, +(___Y, 1)) →* *#(___X, +(___Y, 1))
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (12ms).
| – Problem 2 was processed with processor ForwardNarrowing (2ms).
| | – Problem 3 was processed with processor ForwardNarrowing (0ms).
| | | – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | | | – Problem 5 was processed with processor BackwardInstantiation (1ms).
| | | | | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | | | | – Problem 7 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (0ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| *#(X, +(Y, 1)) | → | *#(1, 0) | | *#(X, +(Y, 1)) | → | *#(X, +(Y, *(1, 0))) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
The following SCCs where found
| *#(X, +(Y, 1)) → *#(X, +(Y, *(1, 0))) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(X, +(Y, 1)) | → | *#(X, +(Y, *(1, 0))) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
The right-hand side of the rule *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, *(1, 0))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| *#(X, +(Y, 1)) | |
| *#(X, +(Y, 0)) | |
Thus, the rule *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, *(1, 0))) is replaced by the following rules:
| *#(X, +(Y, 1)) → *#(X, +(Y, 0)) | *#(X, +(Y, 1)) → *#(X, +(Y, 1)) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(X, +(Y, 1)) | → | *#(X, +(Y, 0)) | | *#(X, +(Y, 1)) | → | *#(X, +(Y, 1)) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
The right-hand side of the rule *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, 0)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, 0)) is deleted.
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| *#(X, +(Y, 1)) | → | *#(X, +(Y, 1)) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
Instantiation
For all potential predecessors l → r of the rule *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, 1)) on dependency pair chains it holds that:
- *#(X, +(Y, 1)) matches r,
- all variables of *#(X, +(Y, 1)) are embedded in constructor contexts, i.e., each subterm of *#(X, +(Y, 1)), containing a variable is rooted by a constructor symbol.
Thus, *
#(
X, +(
Y, 1)) → *
#(
X, +(
Y, 1)) is replaced by instances determined through the above matching. These instances are:
| *#(_X, +(_Y, 1)) → *#(_X, +(_Y, 1)) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| *#(_X, +(_Y, 1)) | → | *#(_X, +(_Y, 1)) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
Instantiation
For all potential predecessors l → r of the rule *
#(
_X, +(
_Y, 1)) → *
#(
_X, +(
_Y, 1)) on dependency pair chains it holds that:
- *#(_X, +(_Y, 1)) matches r,
- all variables of *#(_X, +(_Y, 1)) are embedded in constructor contexts, i.e., each subterm of *#(_X, +(_Y, 1)), containing a variable is rooted by a constructor symbol.
Thus, *
#(
_X, +(
_Y, 1)) → *
#(
_X, +(
_Y, 1)) is replaced by instances determined through the above matching. These instances are:
| *#(__X, +(__Y, 1)) → *#(__X, +(__Y, 1)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| *#(__X, +(__Y, 1)) | → | *#(__X, +(__Y, 1)) |
Rewrite Rules
| *(X, +(Y, 1)) | → | +(*(X, +(Y, *(1, 0))), X) | | *(X, 1) | → | X |
| *(X, 0) | → | X | | *(X, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +
Strategy
Instantiation
For all potential predecessors l → r of the rule *
#(
__X, +(
__Y, 1)) → *
#(
__X, +(
__Y, 1)) on dependency pair chains it holds that:
- *#(__X, +(__Y, 1)) matches r,
- all variables of *#(__X, +(__Y, 1)) are embedded in constructor contexts, i.e., each subterm of *#(__X, +(__Y, 1)), containing a variable is rooted by a constructor symbol.
Thus, *
#(
__X, +(
__Y, 1)) → *
#(
__X, +(
__Y, 1)) is replaced by instances determined through the above matching. These instances are:
| *#(___X, +(___Y, 1)) → *#(___X, +(___Y, 1)) |