![]() |
RFC Matchbounds |
![]() |
AProVE Help System → Techniques → Techniques working on TRSs → | RFC Matchbounds |
We define R# to be the union of R and the string rewrite system, where for each rule a1a2...an → r ∈ R, we have the set of all rules { a1a2...ai# → r | 0 ≤ i < n }.
We define match(R) to be the (infinite) string rewrite system, where for each rule a1a2...an → b1b2...bn ∈ R, we have the set of all rules { (a1, i1)(a2, i2)...(an, in) → (b1, j)(b2, j)...(bn, j) | j = 1 + min(i1, ..., in) }
To prove termination of R, a certificate automaton is constructed, which is closed under rewriting of match(R#). Initially, this automaton is constructed to recognize the set T of all strings (b1, 0)(b2, 0)...(bn, 0)(#, 0)k for all l → b1b2...bn ∈ R. If after the closure, the automaton is finite, the highest match height occurring in the automaton is the match bound of R on T. As all string rewrite systems are trivially right-linear, this match bound implies the termination of R.