YES
The TRS could be proven terminating. The proof took 307 ms.
The following DP Processors were used
Problem 1 was processed with processor BackwardsNarrowing (2ms).
| – Problem 2 was processed with processor BackwardsNarrowing (1ms).
Problem 1: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, b, X) | → | f#(X, X, X) |
Rewrite Rules
| f(a, b, X) | → | f(X, X, X) | | c | → | a |
| c | → | b |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = ∅
μ(f) = μ(f#) = {1, 3}
The left-hand side of the rule f
#(a, b,
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 |
|---|
| f#(c, b, X) | |
Thus, the rule f
#(a, b,
X) → f
#(
X,
X,
X) is replaced by the following rules:
| f#(c, b, X) → f#(X, X, X) |
Problem 2: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(c, b, X) | → | f#(X, X, X) |
Rewrite Rules
| f(a, b, X) | → | f(X, X, X) | | c | → | a |
| c | → | b |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = ∅
μ(f) = μ(f#) = {1, 3}
The left-hand side of the rule f
#(c, b,
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
#(c, b,
X) → f
#(
X,
X,
X) is deleted.