 In the rules for logical operations, the formulae highlighted in the premises are called the minor formulae of that inference, while the formula highlighted in the conclusion is the principal formula of that inference. The other formulae of an inference are called side formulae. A proof (also known as a deduction or derivation) \(\cD\) is a tree of sequents satisfying the conditions that (i) the topmost sequents of \(\cD\) are logical axioms and (ii) every sequent in \(\cD\) except the lowest one is an upper sequent of an inference whose lower sequent is also in \(\cD\). A sequent \(\Gamma \Rightarrow \Delta\) is deducible if there is a proof having \(\Gamma \Rightarrow \Delta\) as its bottom sequent.