 The initial sequents of an \(\mathcal{L}\)-proof (the leaves of the tree) are identity sequents of the form \(\phi \vdash \phi\) (this corresponds to the way arbitrary assumptions can be used as leaves in \(\mathcal{N}\)-proofs), and sequents at lower nodes follow by rules of inference from the sequents at the one or two nodes immediately above them. The rules are of two kinds. First, structural rules for managing lists: Interchange (embodying the idea that the order of the formulas in a list is irrelevant), Contraction (allowing the elimination of duplicate copies of a formula from the list), and Thinning (in the sense of watering down: extra formulas may be added to a list). Second, logical rules associated with the different connectives (and quantifiers): two for each  operator[19],  dealing with the operator in antecedent formulas and in succedent formulas. The rules for succedent occurrences of the operators are analogous to the Introduction rules of natural deduction: thus, for example, the right-hand rule for \(\land\) allows us to infer a sequent