\begin{frame}{Example (3)}

  \vspace*{-1ex}
  \begin{exampleblock}
    {\black{$\asetfuncs = \setexp{\const{e}{\scriptstyle /0},\,
                                  \sbinfunc{\boldsymbol{\cdot}}{\scriptstyle /2}}$, $\,$
            $\asetpreds = \setexp{\sbinpred{\le}{\scriptstyle /2}}$}}
  
    \uncover<2->{%
    We consider a model $\model{\amodel}$ with:}
    \begin{itemize}\vspace*{0.4ex}\setlength{\itemsep}{0.4ex}
      \item<2->
        universe $\model{\bdomain} = \descsetexp{s}{\text{$s$ is binary string}}$
      \item<4->
        interpretation operation $(\boldsymbol{\cdot})^{\model{\amodel}}\,$:
    \begin{itemize}        
      \item<4->  
        $\const{e}$ is interpreted as the empty string $\epsilon$
        \begin{itemize}
          \item
            $\intin{\const{e}}{\model{\amodel}} = \text{empty string $\epsilon$}$
        \end{itemize}
      \item<5->
        $\mathrel{\sbinfunc{\boldsymbol{\cdot}}}$ is interpreted as concatenation of strings
        \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex}
          \item
            $\intin{\sbinfunc{\boldsymbol{\cdot}}}{\model{\amodel}} \funin \bdomain\times\bdomain \to \bdomain,
              \;\; 
                a_0\cdots a_n \mathrel{\intin{\boldsymbol{\cdot}}{\model{\amodel}}} b_0\cdots b_m 
                  = 
                a_0 \cdots a_n b_0 \cdots b_m$ 
            \\[0.25ex]
            e.g.: $\,$
                         $01 \mathrel{\intin{\sbinfunc{\boldsymbol{\cdot}}}{\model{\amodel}}} 100
                           =
                          01100$        
        \end{itemize}
      \item<6->
        $s_1 \mathrel{\sbinpred{\le}} s_2$ is interpreted as: $s_1$ is a prefix of $s_2$ 
        \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex}
          \item
            $\intin{\sbinpred{\le}}{\model{\amodel}} = \descsetexp{\pair{s_1}{s_2}}{\text{$s_1$ is a prefix of $s_2$}}$ 
            \\[0.25ex]
            e.g.: $\,$
               $01 \mathrel{\intin{\sbinpred{\le}}{\model{\amodel}}} 01100$
        \end{itemize}
    \end{itemize}    
    \end{itemize}    
    \pause{}
  \end{exampleblock}
  \pause{}
  
  \uncover<3->{%
  We will be interested in interpreting in $\model{\amodel}$ formulas like:}
  \begin{itemize}
    \item<7->
      $\formula{\existsst{y}{\forallst{x}{\, (y \mathrel{\sbinpred{\le}} x) }}}\,$:
      \hspace*{1.5ex}
      \parbox{0.52\textwidth}
                {\small \sentence{there is a binary string that is prefix}\\[-0.3ex] \hspace*{\fill}\sentence{of every binary string}}
    \item<3->
      $\formula{\forallst{x}{\, (x \mathrel{\sbinpred{\le}} {x \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e}}) }}:$
      \hspace*{1.5ex}
      \sentence{{\small every binary string is a prefix of \ldots}}
  \end{itemize}
\end{frame}

\theme{Interpretation}