Next: Arbitraryness
Up: Approx Trs Menu
 Previous: Membership to CBN
 
As shown in [5], 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 
   WN
   WN
.
Use the command WNo(S,G,F) = WNo(S,F)  for that purpose.
 
Irene DURAND 
2005-02-01