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