325/365
\begin{frame}
  \frametitle{Termination for  $\rewlex{\arel}$ \emph{via} termination of $\trsllex$}
  
  But $\trslex$  is in general not terminating, e.g. if $\symsum > \symsuc$, then
  \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*}
  \pause\smallskip
  
  Starred symbol $\sxmsum$ is `used' infinitely often.
  \pause\medskip

  This is essential in \emph{any} infinite reduction!
  \pause\bigskip
  
  Idea:
  \begin{itemize}
    \item use \alert{numbers instead of stars},
    \item the numbers fix how often a symbol can be used.
  \end{itemize}
  \smallskip\pause
  
  $\Rightarrow$ Yields a terminating TRS $\alert{\itrsllex{\arel}}$.
\end{frame}