 As per usual, the price one has to pay for rules with infinitely many premises is that derivations become infinite (well-founded) trees. The length of a derivation can then be measured by the ordinal rank associated with the tree. One also wants to keep track of the complexity of cuts in the derivation. The length we assign to a formula A, \(\lvert A\rvert\), measures its complexity. It is an ordinal of the form \(\omega\cdot \alpha+n\) where \(\alpha\) is the level of A and \(n&lt;\omega\). One then defines a notion of derivability in \({{\bRA}}\), 