Normalizability

With the Normalizability command, one may check whether a term is normalizable with regard to the approximated TRS.
To check whether a redex in a term is needed in a term (according to the current TRS and approximation), just enter the term where the redex has been replaced with the o symbol and check whether it is normalizable.