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