TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60019 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (29ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (339ms).
| | – Problem 3 was processed with processor ForwardNarrowing (2ms).
| | | – Problem 4 was processed with processor ForwardNarrowing (1ms).
| | | | – Problem 5 was processed with processor ForwardInstantiation (3ms).
| | | | | – Problem 6 remains open; application of the following processors failed [Propagation (0ms), ForwardNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (1ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| times#(x, plus(y, 1)) | → | times#(x, plus(y, times(1, 0))) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| times#(x, plus(y, 1)) | → | plus#(times(x, plus(y, times(1, 0))), x) | | times#(x, plus(y, 1)) | → | times#(1, 0) |
| times#(x, plus(y, 1)) | → | times#(x, plus(y, times(1, 0))) | | times#(x, plus(y, 1)) | → | plus#(y, times(1, 0)) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Strategy
The following SCCs where found
| times#(x, plus(y, 1)) → times#(1, 0) | times#(x, plus(y, 1)) → times#(x, plus(y, times(1, 0))) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| times#(x, plus(y, 1)) | → | times#(1, 0) | | times#(x, plus(y, 1)) | → | times#(x, plus(y, times(1, 0))) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Strategy
Polynomial Interpretation
- 0: 0
- 1: 0
- plus(x,y): 2x + 1
- times(x,y): 0
- times#(x,y): 2y
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| times#(x, plus(y, 1)) | → | times#(1, 0) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| times#(x, plus(y, 1)) | → | times#(x, plus(y, times(1, 0))) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Strategy
The right-hand side of the rule times
#(
x, plus(
y, 1)) → times
#(
x, plus(
y, times(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 |
|---|
| times#(x, plus(y, 0)) | |
Thus, the rule times
#(
x, plus(
y, 1)) → times
#(
x, plus(
y, times(1, 0))) is replaced by the following rules:
| times#(x, plus(y, 1)) → times#(x, plus(y, 0)) |
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| times#(x, plus(y, 1)) | → | times#(x, plus(y, 0)) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Strategy
The right-hand side of the rule times
#(
x, plus(
y, 1)) → times
#(
x, plus(
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 |
|---|
| times#(x, _x31) | |
Thus, the rule times
#(
x, plus(
y, 1)) → times
#(
x, plus(
y, 0)) is replaced by the following rules:
| times#(x, plus(_x31, 1)) → times#(x, _x31) |
Problem 5: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| times#(x, plus(_x31, 1)) | → | times#(x, _x31) |
Rewrite Rules
| times(x, plus(y, 1)) | → | plus(times(x, plus(y, times(1, 0))), x) | | times(x, 1) | → | x |
| plus(x, 0) | → | x | | times(x, 0) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: plus, 1, 0, times
Strategy
Instantiation
For all potential successors l → r of the rule times
#(
x, plus(
_x31, 1)) → times
#(
x,
_x31) on dependency pair chains it holds that:
- times#(x, _x31) matches l,
- all variables of times#(x, _x31) are embedded in constructor contexts, i.e., each subterm of times#(x, _x31) containing a variable is rooted by a constructor symbol.
Thus, times
#(
x, plus(
_x31, 1)) → times
#(
x,
_x31) is replaced by instances determined through the above matching. These instances are:
| times#(x, plus(plus(__x31, 1), 1)) → times#(x, plus(__x31, 1)) |