Problem 1: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(0, 1, x) | → | f#(x, x, x) |
Rewrite Rules
| f(0, 1, x) | → | f(x, x, x) | | f(x, y, z) | → | 2 |
| 0 | → | 2 | | 1 | → | 2 |
Original Signature
Termination of terms over the following signature is verified: f, 2, 1, 0
Strategy
The left-hand side of the rule f
#(0, 1,
x) → f
#(
x,
x,
x) is backward 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
#(0, 1,
x) → f
#(
x,
x,
x) is deleted.