ABSTRACT
Consider finally the case that b = pVq . Replace, for every node h in T , the sequent N h = > c at h by p ,N hf b = > c where N hf b arises from N h by remo ving the the unique predecessor of the occurrence of b . A lso, if N h = } c is the conclusion of a Ev rule with principal formula b , then remove the entire subderivation leading to the right upper neighbour of h . In the resulting object the instances of rules, not using a predecessor as principal occurrence, remain such instances. Instances of Ev with a predecessor as principal occurrence
p ,PVq,Nh’ = 4 p q ,p Vq ,N h' =}> c hprOTTlp P .P .N h’ = > c PV q ,N h’ = * c beC° me P ,N h’ = 4 c
and thus instances of (RC ) together w ith (R P ). I so have proved the inver sion rule
So far, the inversion rules (J E -) have been proved only for K UP . But now the operators, presented in Lemma 1 and Lemma 2, perm it to translate bet ween derivations of the three calculi, and so the inversion rules hold true also for them. It w ill be a useful exercise for the reader to give explicit proofs the case of K SP in the situations when the parameter tree of b is a proper subtree of T .
