|
Reversal |
|
Description
Instead of showing termination of P-chains over R for a given SCC, if P and R are string rewrite systems,
it is sufficient to show termination for (P ∪ R)rev = { lrev → rrev | l → r ∈ P ∪ R }.
Instead of returning (P ∪ R)rev, the Reversal processor returns all SCCs of the
dependency pair graph of (P ∪ R)rev.
Here, for any string s = a1a2...an-1an the reverse
of s is defined as srev = anan-1...a2a1.
Application and Configuration
There is no configuration possible. One should apply this technique for SCCs for which P and R are string rewrite systems, i.e.
term rewrite systems where all function symbols have at most arity 1.
This technique is especially useful in combination with RFC Matchbounds.