Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 7 / a / ii / Solution

A common-context sequent version of the disjunction elimination rule isThe second and third premises record exactly the two boxed subproofs of the natural deduction presentation. Their additional case assumptions do not occur in the conclusion: that is assumption discharge. The surrounding context $\Gamma$ remains throughout. A formulation with different surrounding contexts is equivalent after retaining their union by weakening.