\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}