  The classical calculus has the property, mentioned above, of  height-preserving invertibility of its logical rules. Albert Dragalin refined in the late 1970s the calculus into one in which the  structural rules are moreover “height-preserving  admissible”, meaning that whenever the premiss of such a rule  is derivable, the conclusion is derivable without the rule and with  at most the same size (maximum number of rule instances in a  derivation branch) of derivation. This property has profound effects  on cut elimination: in permuting cut up, Gentzen had to restore the  original contexts (the Γ's and Δ's) through weakenings  and contractions. With the height-preserving admissibility of these  rules, the size of a derivation does not increase when the rules are  applied. Dragalin gave also an intuitionistic multisuccedent calculus with the same type of admissibility of the structural rules.  Troelstra, finally, gave in the textbook Basic Proof Theory  (2000, first ed. 1996) a single-succedent intuitionistic calculus  with height-preserving admissibility of weakening and contraction.  The contraction-free sequent calculi are powerful tools for the  analysis of formal derivations. Many difficult research results in  logic become just exercises through the control over the structure of proofs that the G3-calculi permit.