\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}