The TRS could be proven non-terminating. The proof took 571 ms.
The following reduction sequence is a witness for non-termination:
+#(1, ___x) →* +#(1, ___x)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor ForwardNarrowing (3ms).
| | – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | | – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | | | – Problem 5 was processed with processor BackwardInstantiation (1ms).
| | | | | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| +#(1, x) | → | +#(+(0, 1), x) | | +#(1, x) | → | +#(0, 1) |
Rewrite Rules
| +(1, x) | → | +(+(0, 1), x) | | +(0, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: 1, 0, +
Strategy
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
The following SCCs where found
| +#(1, x) → +#(+(0, 1), x) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(1, x) | → | +#(+(0, 1), x) |
Rewrite Rules
| +(1, x) | → | +(+(0, 1), x) | | +(0, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: 1, 0, +
Strategy
Parameters
- Use original terms restriction: true
- Narrowing normal form lookahead: 2
The right-hand side of the rule +
#(1,
x) → +
#(+(0, 1),
x) 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 |
|---|
| +#(1, x) | |
Thus, the rule +
#(1,
x) → +
#(+(0, 1),
x) is replaced by the following rules:
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| +(1, x) | → | +(+(0, 1), x) | | +(0, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: 1, 0, +
Strategy
Instantiation
For all potential predecessors l → r of the rule +
#(1,
x) → +
#(1,
x) on dependency pair chains it holds that:
- +#(1, x) matches r,
- all variables of +#(1, x) are embedded in constructor contexts, i.e., each subterm of +#(1, x), containing a variable is rooted by a constructor symbol.
Thus, +
#(1,
x) → +
#(1,
x) is replaced by instances determined through the above matching. These instances are:
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| +(1, x) | → | +(+(0, 1), x) | | +(0, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: 1, 0, +
Strategy
Instantiation
For all potential predecessors l → r of the rule +
#(1,
_x) → +
#(1,
_x) on dependency pair chains it holds that:
- +#(1, _x) matches r,
- all variables of +#(1, _x) are embedded in constructor contexts, i.e., each subterm of +#(1, _x), containing a variable is rooted by a constructor symbol.
Thus, +
#(1,
_x) → +
#(1,
_x) is replaced by instances determined through the above matching. These instances are:
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| +(1, x) | → | +(+(0, 1), x) | | +(0, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: 1, 0, +
Strategy
Instantiation
For all potential predecessors l → r of the rule +
#(1,
__x) → +
#(1,
__x) on dependency pair chains it holds that:
- +#(1, __x) matches r,
- all variables of +#(1, __x) are embedded in constructor contexts, i.e., each subterm of +#(1, __x), containing a variable is rooted by a constructor symbol.
Thus, +
#(1,
__x) → +
#(1,
__x) is replaced by instances determined through the above matching. These instances are:
| +#(1, ___x) → +#(1, ___x) |