\begin{frame}[t] \frametitle{Case (b) and (b'): Nested redexes} \begin{minipage}{.5\textwidth} \includegraphics[width=.90\textwidth]{../graphics/critpairlemma}\\[3ex] \end{minipage} \begin{minipage}{.49\textwidth} Assume that $s_1$ is \alert{nested below} $s_0$ in $t$: \pause \begin{itemize} \item $s_0$ be position $p_0$ with rule $\ell \to r$ \item $s_1$ at position $p_1$ \end{itemize} \pause Then \alert{$p_1 = p_0 q q'$} where $\alert{\ell|_q = x} \in \mathcal{X}$. \medskip\pause Let $C = t[\Box]_{p_0}$, then for some $\sigma$: \begin{itemize} \item $t = C[\ell \sigma] \stackrel{s_0}{\to} C[r\sigma] = t_0$ \pause \item $t \stackrel{s_1}{\to} t_1$ (below position $p_0q$) \end{itemize} \pause Let $\tau = \sigma$, except $\tau(x) = t_1|_{p_0q}$. Then \begin{itemize} \item $t|_{p_0q} = \sigma(x) \to \tau(x) = t_1|_{p_0q}$ \end{itemize} \pause Then\vspace{-1ex} \begin{align*} t_0 = C[r\sigma] \to^* &C[r\tau]\\ \leftarrow &C[\ell\tau] \leftarrow^* t_1 \leftarrow C[\ell\sigma] = t \end{align*} \medskip \end{minipage} \end{frame}