\begin{frame}
  \frametitle{Termination of $\trslex$ and $\trsllex$}
  
  Hence we have proven:
  \begin{theorem}
  \centerline{$\airew{{\itrsllex{\arel}}}$ is terminating}
  \end{theorem}
  
  \bigskip
  \pause
  
  \begin{corollary}
  \centerline{$\reltra{\airew{\trslex}}$ is terminating on $\trmover{\setsum{\asig}{\aTrmvar}}$}
  \end{corollary}
  \bigskip
  
  {\bf Proof.} $\reltra{\airew{\trslex}}$ and
  $\reltra{\airew{\trsllex}}$ coincide
  on $\trmover{\setsum{\asig}{\aTrmvar}}$
\end{frame}