left

Rule Reversal

right
AProVE Help SystemTechniquesTechniques working on TRSsRule Reversal

Description

Instead of showing termination for a given TRS R, for string rewrite systems it is sufficient to show termination for Rrev = { lrev → rrev | l → r ∈ R }.

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 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.