If one wants to prove innermost-termination of a TRS R this techniques tries to
remove those rules that can never be applied in innermost reductions. The criterion used is that a rule
l → r of R can be removed if a proper subterm of l can be rewritten.
Application and Configuration
There is no configuration possible.
This technique is always used repeatedly: if one can remove some rules then the
technique is tried directly again afterwards until it finally cannot be applied further.
One should use this technique as a fast preprocessor on TRSs. Its application does not cost much time
and one may get rid of some rules.