\begin{frame}
  \frametitle{$\trslex$ and $\trsllex$}
  
  \begin{theorem}
   \vspace{-1em}
   \begin{center} 
    $\reltra{\airew{{\itrslex{\arel}}}}$ and
    $\reltra{\airew{{\itrsllex{\arel}}}}$ 
    coincide on 
    $\trmover{\setsum{\asig}{\aTrmvar}}$ 
    \end{center}
    \vspace{-1em}
  \end{theorem}
  \medskip\pause
  
  Note that the infinite reduction
  \begin{align*}
    \symsuma{\atrmvar}{\btrmvar} 
    &\myairew{\text{put}} \sxmsuma{\atrmvar}{\btrmvar}\\
    &\myairew{\text{copy}} \symsuca{\sxmsuma{\atrmvar}{\btrmvar}}\\
    &\myairew{\text{copy}} \symsuca{\symsuca{\sxmsuma{\atrmvar}{\btrmvar}}}\\
    &\ldots
  \end{align*}
  \vspace{-2em}
  
  cannot be lifted:
  \begin{align*}
    \symsuma{\atrmvar}{\btrmvar} 
    &\myairew{\text{put}} \lsymsuma{?}{\atrmvar}{\btrmvar}\\
    &\myairew{\text{copy}} \symsuca{\lsymsuma{?-1}{\atrmvar}{\btrmvar}}\\
    &\myairew{\text{copy}} \symsuca{\symsuca{\lsymsuma{?-2}{\atrmvar}{\btrmvar}}}\\
    &\ldots
  \end{align*}
\end{frame}