\begin{frame}
  \frametitle{Towards a Proof of Combinatorial Completeness}
  
  \begin{definition}[Abstraction of $x$]
  \begin{enumerate}
  \item $[x]t= Kt$,
  if $t$ is a constant or a variable other than $x$\\
  \item $[x]x= I$
  \item $[x]tt'= S([x]t)([x]t')$.
  %, if (i) does not apply
  \end{enumerate}\pause
  For $[x_1]([x_2](\ldots ([x_n]t)\ldots ))$ we will write $[x_1x_2\ldots x_n]t$
  \end{definition}
  \pause
  
  Hint: $[x]t= Kt$ can also be used if $t$ does not contain $x$.
  \pause

  \begin{example}
    Let $t= [y]yx$ and $t'= [xy]yx$. Then
    \begin{enumerate}
    \item $
    \begin{array}[t]{l}
    t 
    \pause= S([y]y)([y]x) 
    \pause= SI(Kx),\pause
    \end{array}
    $
    \item<6-> $
    \begin{array}[t]{ll}
    t'
    \pause= [x] t
    \pause= [x](SI(Kx))
    \pause= S([x](SI))([x](Kx))\\
    \ \ \pause= S(K(SI))(S([x]K)([x]x))
    \pause= S(K(SI))(S(KK)I). 
    \end{array}
    $
    \end{enumerate}
  \end{example}
\end{frame}