next up previous
Next: Recognizability Up: Term Menu Previous: Needed redex positions

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.



Irene DURAND
2005-02-01