 The normalization proofs described, turning on applications of the various reductions in a certain order, are moderately complicated in detail, but conceptually elementary: they (like Gentzen’s 1934 proof of the Hauptsatz for sequent calculi) are finitistic in the sense of the Hilbert program. (The corollaries Gentzen derives from the Hauptsatz in the last section of Gentzen (1934), though published after Gödel’s incompleteness theorem, can thus be seen as among the successes of Hilbert’s program.)