ABSTRACT
In this section I consider the calculi K tP or K UP . G iven a derivation D , I shall define, for every occurrence i in the endsequent of D , the predecessors of i together w ith the sequents in D containing such predecessors. I begin by saying that the occurrence in the endsequent is a predecessor of itself, and I proceed in the tree underlying D by recursion on the height of nodes. So consider a sequent s in D which does not lay on a maximal node and thus is conclusion of an instance of a rule. If s does not contain a predeces sor of i then neither shall its prem isses. If s does contain an occurrence j which is predecessor of i then any occurrence in a prem iss which corres ponds to j shall also be a predecessor of i .
