  A second way to apply the sequent calculus is to let sequents that begin derivation branches have, in addition to initial sequents, also the form → A, in which A is an axiom, or an instance of a universal axiom. Now, by Gentzen's “extended Hauptsatz”, cuts in derivations can be permuted up until one of their premisses is an axiom, but these cuts on axioms remain. Another, newer method is to convert axioms into extra rules that are added to the logical rules of sequent calculus, with full cut elimination maintained (as explained in Negri and von Plato 2001, chapter 6, and in Troelstra and Schwichtenberg's 2000, chapter 4.7).