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