\begin{frame}
  \frametitle{Computation with Church Numerals}
  
  \begin{itemize}
    \item $\mathsf{plus} = [m\, n\, f\, x]\; m\, f\, (n\, f\, x)$
    \smallskip
  \pause
    \item $\mathsf{succ} = [n\,f\,x]\; f\, (n\, f\, x)$
    \smallskip
  \pause
    \item $\mathsf{isZero} = [n]\; n \;(K \; \false)\; \true$
    \smallskip
  \pause
    \item $\mathsf{pred} = [n\, f\, x]\; n\; ([g\, h]\; h\, (g\, f)) \; (K x)\; I$
    \smallskip
  \pause
    \item \ldots
  \end{itemize}
  
  \begin{exampleblock}{}
    Idea behind predecessor:
    \begin{align*}
      \mathsf{pred} &= \lambda n.\; \mathsf{fst} \;(n \;f \; z) &
      z &= (0,0) \\
      && f\;(x,y) &= (y,y+1) 
    \end{align*}
    E.g. $\mathsf{pred} \; \overline{3} = \mathsf{fst} \; f(f(f(0,0))) = \mathsf{fst} \; f(f(0,1)) = \mathsf{fst} \; f(1,2) = \mathsf{fst} \; (2,3) = 2$.
  \end{exampleblock}
\end{frame}