\begin{frame} \frametitle{Back and forth between $\trslex$ and $\trsllex$} From $\step_{\trsllex}$ to $\step_\trslex$: \begin{itemize} \item every reduction can be transformed by replacing $\alsymone{\anat}$ by $\asxmone$. \end{itemize} \pause\bigskip From $\step_\trslex$ to $\step_{\trsllex}$: \begin{itemize} \item every finite reduction can be lifted, in particular \item every reduction between two starless terms can be lifted. \end{itemize} \pause\medskip For example: \vspace{-.5em} \begin{align*} \symmula{\atrmvar}{\symsuca{\btrmvar}} &\myairew{\text{put}} \sxmmula{\atrmvar}{\symsuca{\btrmvar}} \myairew{\text{copy}} \symsuma{\sxmmula{\atrmvar}{\symsuca{\btrmvar}}}{\sxmmula{\atrmvar}{\symsuca{\btrmvar}}}\\ &\myairew{\text{select}} \symsuma{\atrmvar}{\sxmmula{\atrmvar}{\symsuca{\btrmvar}}} \myairew{\text{lex}} \symsuma{\atrmvar}{\symmula{\atrmvar}{\sxmsuca{\btrmvar}}}\\ &\myairew{\text{select}} \symsuma{\atrmvar}{\symmula{\atrmvar}{\btrmvar}} \end{align*} \vspace{-2.0em} becomes: \begin{align*} \symmula{\atrmvar}{\symsuca{\btrmvar}} &\myairew{\text{put}} \lsymmula{\emph{2}}{\atrmvar}{\symsuca{\btrmvar}} \myairew{\text{copy}} \symsuma{\lsymmula{\emph{1}}{\atrmvar}{\symsuca{\btrmvar}}}{\lsymmula{\emph{1}}{\atrmvar}{\symsuca{\btrmvar}}}\\ &\myairew{\text{select}} \symsuma{\atrmvar}{\lsymmula{\emph{1}}{\atrmvar}{\symsuca{\btrmvar}}} \myairew{\text{lex}} \symsuma{\atrmvar}{\symmula{\atrmvar}{\lsymsuca{\emph{0}}{\btrmvar}}}\\ &\myairew{\text{select}} \symsuma{\atrmvar}{\symmula{\atrmvar}{\btrmvar}} \end{align*} \vspace{-.5em} \end{frame}