67/365
\begin{frame}
  \frametitle{Monotone $\Sigma$-algebras}
  
  A function $[f]$ is \emph{monotone} (w.r.t.\ ${>}$) if
  \\ \parspace
  \centerline{$a > b$ implies $[f](\ldots,a,\ldots) \; > \; [f](\ldots,b,\ldots)$}
  \smallskip
  \pause
  
  \begin{definition}
  A \alert{well-founded monotone $\Sigma$-algebra $(A,\lbrack \cdot \rbrack,{>})$}:
  \begin{itemize}
  \item a $\Sigma$-algebra $(A,[\cdot])$,
  \item a well-founded order $>$ on $A$\\ (no infinite chains $a_1 > a_2 > \ldots$),
  \item such that for all $f \in \Sigma$ the function $[f]_\AA$ is monotone.
  \end{itemize}
  \end{definition}
  \pause
  \medskip
  
  Relation \alert{$>_\AA$} on terms:
  \alert{$s > t$ if $[s,\alpha] > [t,\alpha]$
  for all assignments $\alpha$}.
  
  \pause
  \begin{lemma}
  \smallskip
  $>_\AA$ is a reduction order for every well-founded monotone $\Sigma$-algebra
  $(A,\lbrack \cdot \rbrack,{>})$
  \end{lemma}
\end{frame}