242/270
\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}