Next: Recognizability
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.
 
Irene DURAND 
2005-02-01