Given an SCC P over a TRS R this techniques tries to find a Ce-compatible reduction order > with
l ≥ r for all l → r ∈ U(P) and s ≥ t for all DPs s → t ∈ P.
If this succeeds it removes all rules that are not in U(P) and it removes all rules and DPs l → r that
are strictly decreasing (l > r) or
where l contains symbols not occurring in any right-hand sides of U(P) ∪ P (l ∉ T(Σ,V))
Here, Σ is the signature of all right-hand sides of U(P) ∪ P.
After the removal the Dependency Graph for the remaining DPs and rules is computed again.
The set of SCCs of this new graph over the new set of rules is the final result of this technique.
A slightly weaker variant of this technique is described in [TGSK '04].
Application and Configuration
AProVE always uses linear polynomial orders as reduction orders for this technique.
The user can configure the maximum value of the coefficients with the range-spinner.
This technique is always used repeatedly: if one can remove some rules or DPs then the
technique is tried directly again afterwards until it finally cannot be applied further with the
given coefficient-range.
One should use this technique as a fast preprocessor on SCCs. Its application does not cost much time
and one can get rid of many easy SCCs.