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