ABSTRACT
From the remarks made at the end of the previous section, it now follows that the exchange operators and the cut elim ination algorithm A from Theorem 2.1 remain in effect for separated derivations in quantifier calculi w ith r e p . The preparation of derivation w ith a pure endsequent leaves un changed both its length and its cut degree. Hence there holds the
THEOREM 3 Let D be a derivation of a pure endsequent in a calculus em ploying Q -ru les with rep and possibly em ploying cuts. Then A (P (D )) is a derivation without cuts of the same endsequent and of length at most e3 (k ,n).
