left

Reversal

right
AProVE Help SystemTechniquesTechniques working on SCCsReversal

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.