Needed 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.