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.