 The equilibrium in question is explicated by the so-called reduction procedures for the logical operators. These procedures enable one to remove from a proof any sentence occurrence that stands both as the conclusion of an application of an introduction rule and as the major premise of an application of the corresponding elimination rule. Repeated application of the procedures will eventually turn the proof into one that is in normal form—essentially, one that is not eligible for any further application of the  procedures.[43]  The significance of proofs in normal form is that they represent direct deductive routes from their premises to their conclusions. 