\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}