Next: Automata
Up: Using Autowrite
Previous: Needed reduction
The TRS Automata menu, gathers commands to compute
automata related to
the lefthandsides 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
20050201