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