251/365
\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}