\begin{frame}
  \small
  
  \vspace{-1ex}
  
  \begin{definition}
  \smallskip
  \begin{itemize}
  \item
  \alert{$\EE \vDash s \approx t$} \quad %(\alert{$s =_\EE t$}) \quad 
  if equation $s \approx t$ is valid in all models of $\EE$.
  \item<2->
  The \alert{equational theory} of $\EE$ consists of all
  equations $s \approx t$ such that $\EE \vDash s \approx t$.
  \end{itemize}
  \end{definition}
  
  \begin{example}<3->
  \begin{itemize}
  \item
  ES $\EE$
  \vspace{-1ex}
  \[
  \GREEN{\begin{array}{r@{~}c@{~}l}
  \m{0}+y & \approx & y \\[.5ex]
  \m{s}(x)+y & \approx & \m{s}(x+y) 
  \end{array}}
  \]
  \onslide<4->
  \[
  \EE \vDash \GREEN{\m{s}(\m{s}(0)+\m{s(0))} \approx \m{s(s(s(0)))}}
  \qquad\qquad
  \onslide<5->
  \EE \nvDash \GREEN{x+y \approx y+x}
  \]
  \vspace{-3ex}
  \item<6->
  Consider model $\Cc = ( \NN, [\cdot] )$
  with \quad $[0] = 0$, \quad $[s](x) = x$, \quad $[+](x,y) = y$.
  \end{itemize}
  \end{example}
  
  \begin{theorem}<7->[Birkhoff]
  \smallskip
  Equational reasoning is \alert{sound} and \alert{complete}
  \[
  \text{$\forall$ ES $\EE$: \quad $\EE \vdash s \approx t \quad \Longleftrightarrow \quad \EE \vDash s \approx t$
  % ${\approx_\EE} ~=~ {=_\EE}$
  }
  \hspace{4cm}
  \smash{\raisebox{-1.75ex}{%
  \href{http://en.wikipedia.org/wiki/Garrett_Birkhoff}%
  {\includegraphics[height=9ex]{../graphics/birkhoff}}}}
  \]
  \vspace{-3ex}
  \end{theorem}
\end{frame}