29/127
\begin{frame}
  \frametitle{Combinatorial Completeness}

  \begin{lemma}[Combinatorial Completeness]
  Given  CL-term $t$, one can find a CL-term $F$ such that  
  
  
  $$Fx_1\ldots x_n\to^* t$$
  
  This $F$ can be constructed 
  such that the the variables $x_1,\ldots,x_n$ do not occur in $F$.
  \end{lemma}
  \pause
  \bigskip
  
  \onslide<3->{Then closure under substitutions yields:}
  \begin{lemma}
  Then $F\, t_1 \ldots t_n \to^* t[x_1 \mapsto t_1, \dots x_n \mapsto t_n]$
  for arbitrary terms $t_1,\ldots,t_n$.
  \end{lemma}
\end{frame}