 The lines indicate a transition from the upper formula(s) to the one just beneath the line, using the rule of inference indicated on the right edge of the line. (We might replace these horizontal lines with vertical or splitting lines to more clearly indicate tree-branches, and label these branches with the rule of inference responsible, and the result would look even more tree-like). Gentzen uses the numerals on the leaves as a way to keep track of subproofs. Here the antecedent of the conditional to be proved is entered (twice, since there are two separate things to do with it) with the numeral ‘1’, the antecedent of the consequent of the main theorem is entered with numeral ‘2’, and the formula \(\neg r\) (to be used in the reductio part of the proof) is entered with numeral ‘3’. When the relevant “scope changing” rule is applied (indicated by citing the numeral of that branch as part of the citation of the rule of inference, in parentheses) this numeral gets crossed out, indicating that this subproof is finished.