  Gentzen developed and studied the system of natural deduction during  1932, and had arrived by September 1932 at a calculus of natural  deduction (ND for short) that is standard today. By this time, he had noticed that if an introduction, say a derivation of  A &amp; B from A and B separately,  is followed by the corresponding elimination, say a derivation of  A, the formula A &amp; B constitutes a local maximum, a “hillock”, that can be eliminated. He also  called such hillocks “detours”, and what is now called a  detour conversion removes such unnecessary pairs of  introduction-elimination steps. The result of the steps of  “normalization” is a derivation in “normal  form”.