[proofplan] The proof is a direct verification of the local computation rule for disjunction. In a left-introduction detour, the major premise of $\vee E$ is known to have been introduced from the left disjunct $A$, so the elimination can enter the left case derivation immediately. Substitution of the derivation of $A$ for the discharged assumption $A$ produces a derivation of the same conclusion $C$, while the unused right branch is removed. The right-introduction case is identical with the roles of $A$ and $B$ interchanged. [/proofplan] [step:Reduce the left introduction detour to the left case derivation] Consider the derivation \begin{align*} \mathcal{D}_L = \frac{ \frac{\Pi_A}{A}\ \vee I_1 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E. \end{align*} The major premise of the final $\vee E$ inference is the formula $A \vee B$, and this formula was introduced by $\vee I_1$ from the derivation $\Pi_A$ of $A$. Therefore the local computation rule for $\vee E$ after $\vee I_1$ selects the left case derivation $\Delta_A$. Define $\Delta_A[\Pi_A/A]$ to be the derivation obtained from $\Delta_A$ by replacing each occurrence of the distinguished open assumption $A$ discharged by $\vee E$ with a copy of the derivation $\Pi_A$. Since $\Delta_A$ derives $C$ from that distinguished assumption $A$, and since $\Pi_A$ derives $A$, the substitution produces a well-formed derivation of $C$. Thus \begin{align*} \mathcal{D}_L \longrightarrow \Delta_A[\Pi_A/A]. \end{align*} The branch $\Delta_B$ is removed in this reduction because the introduced disjunction came from the left disjunct and the right case is not inspected in this local computation. [guided] We examine the left-introduction detour: \begin{align*} \mathcal{D}_L = \frac{ \frac{\Pi_A}{A}\ \vee I_1 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E. \end{align*} The final rule is [disjunction elimination](/theorems/4625). Its major premise is $A \vee B$, and its two case derivations say: if $A$ is assumed, $\Delta_A$ derives $C$; if $B$ is assumed, $\Delta_B$ derives $C$. The special feature of this derivation is that the major premise $A \vee B$ was not obtained from arbitrary information. It was introduced immediately by $\vee I_1$ from a derivation $\Pi_A$ of $A$. Hence the disjunction contains no genuine case distinction at this point: locally, the proof already knows that the left disjunct is the one that was supplied. The reduction therefore enters the left branch directly. Define $\Delta_A[\Pi_A/A]$ to be the derivation obtained from $\Delta_A$ by replacing every occurrence of the distinguished discharged assumption $A$ with a copy of the derivation $\Pi_A$. This operation is well formed because the replaced nodes have formula $A$, and $\Pi_A$ is a derivation of exactly $A$. After replacement, the open occurrences of the distinguished assumption $A$ have been closed by $\Pi_A$, and the conclusion of the branch remains $C$. Therefore $\Delta_A[\Pi_A/A]$ is a derivation of $C$. Thus the left detour reduces as \begin{align*} \frac{ \frac{\Pi_A}{A}\ \vee I_1 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E \longrightarrow \Delta_A[\Pi_A/A]. \end{align*} The right branch $\Delta_B$ is discarded because it corresponds to the case $B$, while the immediately preceding introduction supplied the case $A$. [/guided] [/step] [step:Reduce the right introduction detour to the right case derivation] Consider the derivation \begin{align*} \mathcal{D}_R = \frac{ \frac{\Pi_B}{B}\ \vee I_2 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E. \end{align*} The major premise of the final $\vee E$ inference is again $A \vee B$, but now it was introduced by $\vee I_2$ from the derivation $\Pi_B$ of $B$. Therefore the local computation rule for $\vee E$ after $\vee I_2$ selects the right case derivation $\Delta_B$. Define $\Delta_B[\Pi_B/B]$ to be the derivation obtained from $\Delta_B$ by replacing each occurrence of the distinguished open assumption $B$ discharged by $\vee E$ with a copy of the derivation $\Pi_B$. Since $\Delta_B$ derives $C$ from that distinguished assumption $B$, and since $\Pi_B$ derives $B$, the substitution produces a well-formed derivation of $C$. Thus \begin{align*} \mathcal{D}_R \longrightarrow \Delta_B[\Pi_B/B]. \end{align*} The branch $\Delta_A$ is removed because the introduced disjunction came from the right disjunct. [guided] The right-introduction detour has the form \begin{align*} \mathcal{D}_R = \frac{ \frac{\Pi_B}{B}\ \vee I_2 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E. \end{align*} As before, the final inference is disjunction elimination. The difference is that the major premise $A \vee B$ was introduced by $\vee I_2$, so it was obtained from a derivation $\Pi_B$ of the right disjunct $B$. Thus the relevant case derivation is now the right branch. Define $\Delta_B[\Pi_B/B]$ to be the derivation obtained from $\Delta_B$ by substituting a copy of $\Pi_B$ for every occurrence of the distinguished discharged assumption $B$. This substitution is well formed because each replaced assumption has formula $B$, and $\Pi_B$ derives $B$. The conclusion of the branch is still $C$, so the substituted derivation derives $C$. Consequently, \begin{align*} \frac{ \frac{\Pi_B}{B}\ \vee I_2 \qquad [A]\ \Delta_A\ C \qquad [B]\ \Delta_B\ C }{ C }\ \vee E \longrightarrow \Delta_B[\Pi_B/B]. \end{align*} The left branch $\Delta_A$ is discarded because this local computation was generated by the right disjunction introduction rule. [/guided] [/step] [step:Conclude that both introduction elimination detours satisfy the stated reductions] The first reduction shows that an immediate $\vee E$ following $\vee I_1$ contracts to substitution into the left case derivation: \begin{align*} \mathcal{D}_L \longrightarrow \Delta_A[\Pi_A/A]. \end{align*} The second reduction shows that an immediate $\vee E$ following $\vee I_2$ contracts to substitution into the right case derivation: \begin{align*} \mathcal{D}_R \longrightarrow \Delta_B[\Pi_B/B]. \end{align*} These are precisely the two disjunction introduction elimination reductions stated in the theorem. [/step]