\begin{frame} \frametitle{Stepwise Termination Proofs} Stepwise termination proofs with monotone $\Sigma$-algebras: \begin{theorem} If there exists a well-founded monotone $\Sigma$-algebra $(A,[\cdot],{>})$ s.t. % \begin{itemize} \item ${R} \subseteq {\ge}$, and \item ${R'} \subseteq {>}$, and \end{itemize} where ${\ge} := {>} \cup {=}$. Then \vspace{-1.5ex} \begin{align*} \SN(R) \implies \SN(R \cup R') \end{align*} \end{theorem} \smallskip This theorem allows us to stepwise remove rules until none are left. \pause\bigskip \begin{remark} Instead of ${\ge}$ we can more generally use a monotone relation $\succeq$ with $\SN({>}/{\succeq})$. \end{remark} \end{frame}