\begin{frame}
  \frametitle{Recursive definition of LPO}
  
  Let $\arel$ be a strict order on signature $\asig$
  \bigskip
  
  { \setlength{\fboxsep}{1.3ex}
  \fbox{\parbox{.9\textwidth}{
  Define $\arel_{\mathit{lpo}}$ on $\trmover{\asig,\aTrmvar}$ by:
  $\atrm \arel_{\mathit{lpo}} \btrm$ iff
  \smallskip
  \begin{list}{}{\setlength{\itemsep}{0cm}\setlength{\parsep}{0cm}}
  \item[\emph{(LPO1)}\;]
    $\setin{\btrm}{\trmvar{\atrm}}$ and $\trmne{\atrm}{\btrm}$, or
  \smallskip
  \item[\emph{(LPO2)}\;]
    $\trmeq{\atrm}{\symonea{\aitrm{\natone},\ldots,\aitrm{\bnat}}}$,
    $\trmeq{\btrm}{\symoneb{\bitrm{\natone},\ldots,\bitrm{\anat}}}$, and
  \smallskip
    \begin{list}{}{\setlength{\itemsep}{0cm}\setlength{\parsep}{0cm}}
    \item[\emph{(LPO2a)}\;] 
      $\exists \natle{\natone}{\natle{\aidx}{\bnat}}$,
      with $\aitrm{\aidx} = \btrm$ or $\aitrm{\aidx} \arel_{\mathit{lpo}} \btrm$, or
  \smallskip
    \item[\emph{(LPO2b)}\;]
      $\asymone \arel \bsymone$ and
      $\atrm \arel_{\mathit{lpo}} \bitrm{\bidx}$
      for all $\natle{\natone}{\natle{\bidx}{\anat}}$, or
  \smallskip
    \item[\emph{(LPO2c)}\;]
      $\symeq{\asymone}{\bsymone}$, and\\[-2ex]
      \begin{changemargin}{1.1cm}{0cm}
      $\atrm \arel_{\mathit{lpo}} \bitrm{\bidx}$ for all $\natle{\natone}{\natle{\bidx}{\anat}}$, and \\
      there exists $\natle{\natone}{\natle{\aidx}{\bnat}}$, s.t.\\
      $\trmeq{\aitrm{\natone}}{\bitrm{\natone}}$, $\ldots$,
      $\trmeq{\aitrm{\natpre{\aidx}}}{\bitrm{\natpre{\aidx}}}$ and
      $\aitrm{\aidx} \arel_{\mathit{lpo}} \bitrm{\aidx}$.
      \end{changemargin}
    \end{list}
  \end{list}
   }}}
  
  \pause
  \begin{theorem}
    \centerline{$\rewlex{\arel}$ is equivalent with $\arel_{\mathit{lpo}}$}
  \end{theorem}
\end{frame}