Up: Approx Trs Menu
Previous: Membership to CBN
As shown in , the sets of terms of
that are normalizable
may be augmented if the signature
is extended with just one fresh constant
symbol (for instance ).
Using the command WN(S,G,F) = WN(S,F) one can check whether signature
extension preserves the set of normalizable terms. If this is not the case,
then a term witnessing that
WN WN is shown.
The same can be done with
as for the growing
approximation we may have
WN WN but
Use the command WNo(S,G,F) = WNo(S,F) for that purpose.