The premisses are either main or minor. A path containing the formula F is called an endpath .
Every derivation contains at least one endpath.
A formula which is the conclusion of an I and a premiss of an E is called a peak . Every derivation in can be reduced to a normal form applying a finite member of reductions. The derivation in normal form has the same endformula and no new undischarged assumptions. We choose a peak of maximum degree which is not below any other peak of the same degree and apply the corresponding reduction. We repeat this operation until there are no peaks left.