\begin{frame}[t] \frametitle{Case (a): Disjoint redexes} \begin{minipage}{.5\textwidth} \includegraphics[width=.90\textwidth]{../graphics/critpairlemma} \end{minipage} \begin{minipage}{.49\textwidth} Assume $s_0$ {and} $s_1$ are \alert{disjoint}. \pause\bigskip Then $t= C[s_0,s_1]$\\ for some $2$-hole context $C$. \pause\bigskip Let $s_0'$, $s_1'$ be the contracta of $s_0$, $s_1$. \bigskip\pause Then $t_0 = C[s_0',s_1]$ and $t_1 = C[s_0,s_1']$. \bigskip\pause Take $t_2 = C[s_0',s_1']$ as common reduct. \end{minipage} \end{frame}