Next: Automata
Up: Using Autowrite
 Previous: Needed reduction
 
The TRS Automata  menu, gathers commands to compute
automata related to
the left-handsides of the current TRS or to its approximation.
The Redex automaton , Reducible automaton ,
Nf automaton  compute the automata recognizing
the sets of redexes, reducible terms, normal forms.
We have the possibilities of computing Toyama's or Jacquemard's 
 automaton recognizing 
with either 
- 
   NF: command Automaton C NF , 
 
- 
: command Automaton C A , 
 
- 
: command Automaton C S , 
 being the instances of the current termset.
 
We can also compute the automaton 
 which
recognizes the set of reducible terms without 
-needed
redex: command Automaton D .
 
Irene DURAND 
2005-02-01