\begin{frame}
  \small
    
  We write $t \ge s$ if $t$ can be obtained from $s$ by overlining some redex positions.

  \begin{definition}[Lifting]
  A $\atrs$ rewrite sequence $A : s_1 \to s_2 \to \ldots \to s_n$
  can be \alert{lifted} if:
  \begin{center}
    \begin{tikzpicture}[thick,node distance=25mm]
      \node (s1) {$s_1$};
      \node [right of=s1] (s2) {$s_2$};
      \node [right of=s2] (sd) {$\ldots$};
      \node [right of=sd] (sn) {$s_n$};
      
      \node [above of=s1,node distance=15mm] (t1) {$t_1$};
      \node [right of=t1] (t2) {$t_2$};
      \node [right of=t2] (td) {$\ldots$};
      \node [right of=td] (tn) {$t_n$};
      
      \begin{scope}[->]
      \draw (s1) -- (s2) node [midway,above] {$\langle \rho_1,\,p_1 \rangle$};
      \draw (s2) -- (sd) node [midway,above] {$\langle \rho_2,\,p_2 \rangle$};
      \draw (sd) -- (sn) node [midway,above] {$\langle \rho_{n-1},\,p_{n-1} \rangle$};

      \draw (t1) -- (t2) node [midway,above] {$\langle \overline{\rho}_1,\,p_1 \rangle$};
      \draw (t2) -- (td) node [midway,above] {$\langle \overline{\rho}_2,\,p_2 \rangle$};
      \draw (td) -- (tn) node [midway,above] {$\langle \overline{\rho}_{n-1},\,p_{n-1} \rangle$};
      \end{scope}

      \path (s1) -- (t1) node [midway,sloped] {$\le$};
      \path (s2) -- (t2) node [midway,sloped] {$\le$};
      \path (sn) -- (tn) node [midway,sloped] {$\le$};
    \end{tikzpicture}
  \end{center}
  for some $\overline{\atrs}$ rewrite sequence $B : t_1 \to \ldots t_n$.
  \end{definition}
  \pause\medskip
  
  \begin{lemma}
    For orthogonal TRSs: a reduction is a development $\quad\Longleftrightarrow\quad$ it can be lifted.
  \end{lemma}
\end{frame}