\begin{frame}
  \frametitle{Church Booleans}
  
  \begin{block}{}
    Church encoding of boolean values \emph{true} and \emph{false}:
    \begin{align*}
      \true &= K    &\pause \true\; x\, y \to^* x\\
      \false &= KI  &\pause \false\; x\, y \to^* y    
    \end{align*}    
  \end{block}
  \pause
  \bigskip
  
  Then we can define:
  \begin{align*}
    \mathsf{or} &= SII 
    & \mathsf{or}\;x\,y &\to (I x) (I x) y \to^* xxy\\
    && \mathsf{or}\;\true\,y &\to^* \true\; \true\; y \to ^* \true\\
    && \mathsf{or}\;\false\,y &\to^* \false\; \false\; y \to ^* y
  \end{align*}
  \pause
  Exercise: define \structure{$\mathsf{and}$} and \structure{$\mathsf{not}$}.\\
  \pause
  \bigskip
  
  If $x$ then $y$ else $z$:
  \begin{align*}
    \mathsf{if} &= \pause I &\pause \mathsf{if}\;\true\,y\,z \to \true\;y\,z \to^* y\\
    &&\pause \mathsf{if}\;\false\,y\,z \to \false\;y\,z \to^* z
  \end{align*}
\end{frame}