 Gentzen saw that this could be generalized, at least for the system for intuitionistic logic. Call the “route straightening” modifications to a derivation described in the previous paragraphs (i.e., deleting the “detour” conjunction or conditional and taking a premiss of the former introduction rule as the conclusion, or obtaining the conclusion by means of argumentation from the subproof for the introduction rule), and analogous modifications for the other operators, an immediate reduction. Then, roughly, his result (now called the Normalization Theorem) is that any derivation can be transformed by a sequence of immediate reductions into a derivation in normal form, in which no (occurrence of) a formula obtained by one of the introduction rules is used as the major premiss of an elimination rule. We give examples of immediate reductions in  figure 6.  This is rough because of an annoying complication in the cases of the elimination rules (\(\lor\)-E, \(\exists\)-E) which involve subproofs.