\begin{frame}[t]{Encoding of Binary Words as Terms}
  The formula $\aformi{\!\forestgreen{I}}$ will be defined over functions and predicate in:
  \begin{talign}
    \asetfuncs = \setexp{\const{e}{\scriptstyle /0},\, \sunfunci{f}{0}{\scriptstyle /1}, \sunfunci{f}{1}{\scriptstyle /1}}
    &&
    \asetpreds = \setexp{\sunpred{P}{\scriptstyle /2}}
  \end{talign}
  \pause   
  We consider the encoding of binary strings into $\asetfuncs$-terms:
  \begin{center}
  \begin{tabular}{|c|c|}
    \hline
    binary word & term encoding \\[-0.25ex]
    \hline\hline
    $\epsilon \;$ \text{(empty word)} & $\const{e}$ \\
    \hline
    $0$         & $\formula{\unfunci{f}{0}{\const{e}}}$ \\
    \hline
    $1$         & $\formula{\unfunci{f}{1}{\const{e}}}$ \\
    \hline
    $01$        & $\formula{\unfunci{f}{0}{\unfunci{f}{1}{\const{e}}}}$ \\
    \hline
    $10$        & $\formula{\unfunci{f}{1}{\unfunci{f}{0}{\const{e}}}}$ \\
    \hline
    $\vdots$    & $\vdots$ \\
    \hline
    $b_1 b_2 \ldots b_{l-1}b_l$ & 
    $\formula{\unfunci{f}{b_1}{\unfunci{f}{b_2}{\ldots\unfunci{f}{b_{l-1}}{\unfunci{f}{b_{l}}{\const{e}}}\ldots}}}$
    \\ 
    \hline
  \end{tabular}  
  \end{center}
  \pause\smallskip
  
  \begin{goal}{}
    For binary word $\alert{w} = b_1 b_2 \ldots b_l$ 
    and $\asetfuncs$-terms $\formula{\ater}$ 
    we abbreviate:
    \begin{talign}
      \formula{\unfunci{f}{\alert{w}}{\ater}}
      \defdby
      \formula{\unfunci{f}{b_1}{\unfunci{f}{b_{2}}{\ldots\unfunci{f}{b_l}{t}\ldots}}}
    \end{talign}
  \end{goal}
\end{frame}