left

Rewriting

right
AProVE Help SystemTechniquesTechniques working on SCCsRewriting

Description

One of the DP transformations only available for innermost-termination is rewriting:
an SCC consisting of pairs P ∪ { s → t } over a set of rules R can be rewritten to Here, U(t) are the usable rules of t.

Application and Configuration

See the more general side about DP transformations.