Up: Term Menu
Previous: Needed redex positions
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.