MAYBE
The TRS could not be proven terminating. The proof attempt took 794 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (5ms), PolynomialLinearRange4 (250ms), DependencyGraph (4ms), ReductionPairSAT (308ms), DependencyGraph (3ms), SizeChangePrinciple (86ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| U12#(c, x) | → | g#(f(c), x) | | g#(x, b) | → | U11#(f(b), x) |
| U11#(x, x) | → | U12#(x, x) |
Rewrite Rules
| f(x) | → | U01(a, x) | | U01(h(y), x) | → | y |
| g(x, b) | → | U11(f(b), x) | | U11(x, x) | → | U12(x, x) |
| U12(c, x) | → | g(f(c), x) | | a | → | h(b) |
| a | → | h(c) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a, h
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(x) | → | a# | | f#(x) | → | U01#(a, x) |
| U12#(c, x) | → | T(x) | | U12#(c, x) | → | g#(f(c), x) |
| U12#(c, x) | → | f#(c) | | g#(x, b) | → | U11#(f(b), x) |
| g#(x, b) | → | f#(b) | | U11#(x, x) | → | U12#(x, x) |
Rewrite Rules
| f(x) | → | U01(a, x) | | U01(h(y), x) | → | y |
| g(x, b) | → | U11(f(b), x) | | U11(x, x) | → | U12(x, x) |
| U12(c, x) | → | g(f(c), x) | | a | → | h(b) |
| a | → | h(c) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a, h
Strategy
Context-sensitive strategy:
μ(b) = μ(c) = μ(a) = μ(a#) = μ(T) = ∅
μ(f) = μ(U11#) = μ(f#) = μ(U12#) = μ(h) = μ(U01) = μ(U11) = μ(U12) = μ(U01#) = {1}
μ(g) = μ(g#) = {1, 2}
The following SCCs where found
| U12#(c, x) → g#(f(c), x) | g#(x, b) → U11#(f(b), x) |
| U11#(x, x) → U12#(x, x) |