Next: TRS Automata
Up: Reduction and Needed Reduction
 Previous: Classical reduction
 
One can perform a needed-reduction step
using the leftmost-outermost needed redex.
The ``Needed reduction to normal form'' command applies the needed strategy
until a normal form is reached 
(may loop if term does not have a normal form).
Use the Stop button (or command) to stop a looping computation.
 
Irene DURAND 
2005-02-01