330/365
\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}