ABSTRACT
For the calculi K SPC and K tPC the Case 3 in the definition of the exchange operator Ej can be sim plified drastically if the cut formula v happens not to occur as parameter in the logical rules leading to the prem isses of the c u t : in this situation, the three given subderivations are replaced by
p ,N u M =$ P P , N ==> u
and the k -cu t is actually removed. W hile such an event is but accidental, a different approach to the operator A 0 will always produce such situations, and I shall discuss this in the next two Lemmata as a m otivation for later developm ents.
