\begin{frame}
  \frametitle{Church Numerals}
  
  \begin{block}{}
    Church encoding of natural numbers: $\overline{n} = \lambda f.\; \lambda x.\; f^n(x)$.
    \pause
    In CL:
    \begin{align*}
      \overline{0} &= KI\\
      \overline{n+1} &= ([nfx]\; f\; (n \;f\;x))\; \overline{n} \pause\approx S\; (S (K S) (S (K K) I))\; \overline{n}  
    \end{align*}    
  \end{block}
  \pause
  \vspace{-2ex}
  
  \begin{align*}
    \overline{0}\; f\, x &\to^* x
  &\pause
    \overline{n+1}\; f\, x 
    &\pause= S\; (S (K S) (S (K K) I))\; \overline{n} \; f \; x\\
    &&&\pause\to S (K S) (S (K K) I)\; f\; (\overline{n} \; f) \; x\\
    &&&\pause\to K S f (S (K K) I\; f)\; (\overline{n} \;f) \; x\\
    &&&\pause\to S (S (K K) I f)\; (\overline{n} \;f) \; x\\
    &&&\pause\to S (K K f (I\; f))\; (\overline{n} \;f) \; x\\
    &&&\pause\to S (K (I\; f))\; (\overline{n} \;f) \; x\\
    &&&\pause\to S (K\; f)\; (\overline{n} \;f) \; x\\
    &&&\pause\to K f x\; (\overline{n} \;f \;x)\\
    &&&\pause\to f (\overline{n} \;f \;x)\\
    &&&\pause\to^* f^{n+1}(x)
  \end{align*}
\end{frame}