ABSTRACT
Now | d | = 1 + | %(e) | , and since \ ls enlarged only in the Cases 2 b , an im m ediate induction shows | x (e) | < ||e ||-2 ; hence \d\ < ||e|| . A lso, C ^ (e)0 and the A k° come from values of f at nodes ep w ith ||ep|| < ||e*i|| whence for the arithm etized sequences C-^(e)°< e 2(b, ||ep||), A k°< e 2(b, ||ep| | ) ; hence max(tf) < e 2(b,n) for the maximum n of | d | and the ||ep| | , n < ||e*i|| . Thus
CkT(d) < e 2(c, n + e 2(b,n)) < e 2( c + b , n) ,
and so f(e*i) is bounded by e 2( c + b , n) where c depends only on CAT and b only on H and J . ]
I now shall introduce a reduction operator Rj which acts upon derivations D and reduces the cut degree by at least 1. Recall that the cut degree cdg{D) of a derivation D was defined globally to be 0 if D contains no cuts, and to be 1 plus the maximum of all degrees of cuts in D otherwise; this can be made into a recursive definition by setting cdg{D) = su p < cdg (D fn) | n cuj> . Observe that, in the situation of Lemma 3 , the continuation of H and J to a derivation D by a cut w ith the formula v of degree |v | would result in cdg (D ) = max( | v | + 1 , cdg (H), cdg( J ) ) . The same endsequent produced by R 0(H ,J ,k j ) requires at most the cut degree m ax(| v | , cd g (H), cd g (J)).
