 Sequent calculus, SC for short, can be seen as a formal representation of the derivability relation in natural deduction. A sequent consists of a list Γ of formulas, an arrow (in Gentzen, later also other markers have been used), and one formula as a conclusion. The list gives the assumptions the conclusion depends on in a derivation, in a local notation where in ND they are found in the leaves of a derivation tree. Gentzen also generalized sequents so that they have, instead of one conclusion, a list of possible cases after the arrow. This novelty led to the first satisfactory formulation of a proof system for classical logic. Gentzen's SC rules for conjunction and implication are, with commas separating elements in lists: