\begin{frame}{Checking Formula Satisfiability in a Model} \begin{exampleblock}{ \black{$\model{\amodel} \satisfies \formula{\forallst{x}{\, (x \mathrel{\sbinpred{\le}} {x \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e}}) }}$} \hspace*{1ex} %where \hspace*{1ex} \begin{minipage}{0.6\textwidth} {\small \begin{itemize} \item \black{universe $\model{\bdomain} = \descsetexp{s}{\text{$s$ is binary string}}$} \item \black{$\intin{\const{e}}{\model{\amodel}} = \text{empty string $\epsilon$}$} \item \black{$\intin{\sbinpred{\boldsymbol{\cdot}}}{\model{\amodel}}\,$: concatenation of strings} %$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$ \item \black{$\intin{\sbinpred{\le}}{\model{\amodel}} = \descsetexp{\pair{s_1}{s_2}}{\text{$s_1$ is a prefix of $s_2$}}$} \end{itemize} } \end{minipage} } \pause{} \vspace*{-1.5ex} \begin{align*} & \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\, (x \mathrel{\sbinpred{\le}} {x \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e}}) }} \;\;\uncover<10->{\alert{\checkmark}} \\ & \uncover<3->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{s}]} \formula{\freevar{x} \mathrel{\sbinpred{\le}} {\freevar{x} \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e}}}$}} \\ & \uncover<4->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\pair{\intin{\freevar{x}}{\model{\amodel},\saluf[\freevar{x}\mapsto \forestgreen{s}]}} {\intin{(\freevar{x} \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e})}{\model{\amodel},\saluf[\freevar{x}\mapsto \forestgreen{s}]}} \in \intin{\sbinpred{\le}}{\model{\amodel}}$}} \\ & \uncover<5->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\pair{\forestgreen{s}} {\intin{\freevar{x}}{\model{\amodel},\saluf[\freevar{x}\mapsto \forestgreen{s}]} \mathrel{\intin{\sbinpred{\boldsymbol{\cdot}}}{\model{\amodel}}} \intin{\const{e}}{\model{\amodel},\saluf[\freevar{x}\mapsto \forestgreen{s}]}} \in \intin{\sbinpred{\le}}{\model{\amodel}}$}} \\ & \uncover<6->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\pair{\forestgreen{s}} {\forestgreen{s} \mathrel{\intin{\sbinpred{\boldsymbol{\cdot}}}{\model{\amodel}}} \intin{\const{e}}{\model{\amodel}}} \in \intin{\sbinpred{\le}}{\model{\amodel}}$}} \\ & \uncover<7->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\pair{\forestgreen{s}} {\forestgreen{s} \mathrel{\intin{\sbinpred{\boldsymbol{\cdot}}}{\model{\amodel}}} \epsilon} \in \intin{\sbinpred{\le}}{\model{\amodel}}$}} \\ & \uncover<8->{ \;\;\;\;\Longleftrightarrow\;\; \text{for all $\forestgreen{s}\in\model{\bdomain}\,$: $\,$ $\pair{\forestgreen{s}}{\forestgreen{s}} \in \intin{\sbinpred{\le}}{\model{\amodel}}$}} \;\;\uncover<9->{\alert{\checkmark}} \end{align*} \uncover<11->{% Hence we have formally established: $\model{\amodel} \satisfies \formula{\forallst{x}{\, (x \mathrel{\sbinpred{\le}} {x \mathrel{\sfunc{\boldsymbol{\cdot}}} \const{e}}) }}$.} \end{exampleblock} \end{frame}