\begin{frame}[t]{Formula Truth in a Model (\alert{Full} Definition)}
  \begin{block}{}
  \emph{Truth} of a formula $\formula{\aform}$ in a model $\model{\amodel}$ with universe $\model{\adomain}$
  {\it with respect to environment $\saluf$}
  is defined by induction on the structure of $\formula{\aform}$:
  %
  \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item<2->    
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\aform}}
       \;\iff\; \model{\amodel} \satisfiesnotlookup{\saluf} \formula{\aform}$
    \item<2->
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logand{\aform}{\bform}}
       \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                \;\text{ and }\;
                \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$
    \item<2->
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logor{\aform}{\bform}}
       \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                \;\text{ or }\;
                \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$                    
    \item<2->
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logimp{\aform}{\bform}}
       \;\iff\; (\text{if }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                 \;\text{ then }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\bform} )$          
    \item<3->
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\narypredsynvar{P}{\ateri{1},\ldots,\ateri{n}}}
       \;\iff\; \tuple{\interpretin{\formula{\ateri{1}}}{\model{\amodel},\saluf},
                       \ldots,
                       \interpretin{\formula{\ateri{n}}}{\model{\amodel},\saluf}} 
                \in \interpretin{\snarypredsynvar{P}}{\model{\amodel}} $  
      \vspace*{-1.5ex}   
      \begin{center}
        \begin{minipage}{0.9\textwidth}
        \uncover<4->{%  
          \begin{block}{}%{interpretation of terms}
            \vspace*{-2.5ex} 
            \begin{align*}  
            \uncover<4->{%
              \intin{\formula{\ater}}{\model{\amodel},\saluf} 
                =
              \begin{cases}
                \aluf{\formula{\avarsynvar}} 
                  & \text{if $\formula{\ater} = \formula{\avarsynvar}$ for a variable $\formula{\avarsynvar}$}
                \\
                \intin{\aconstsynvar}{\model{\amodel}}
                  & \text{if $\formula{\ater} = \aconstsynvar$ for a constant $\aconstsynvar$}
                \\
                \fap{\intin{\safuncsynvar}{\model{\amodel}}}
                    {\intin{\formula{\ateri{1}}}{\model{\amodel},\saluf},
                    \ldots,
                    \intin{\formula{\ateri{n}}}{\model{\amodel},\saluf}}
                  & \text{if $\formula{\ater} = \formula{\afuncsynvar{\ateri{1},\ldots,\ateri{n}}}$}    
              \end{cases}}%  
            \end{align*}
          \end{block}}
         \end{minipage}
      \end{center}
    \smallskip
    \item<5->  
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\aform}}
       \;\iff\; \text{for all $\forestgreen{a} \in \model{\adomain}$ it holds: }
                \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform}$    
    \item<6->      
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\aform}}
       \;\iff\; \text{for some $\forestgreen{a} \in \model{\adomain}$ it holds: }
                \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform}  $    
  \end{itemize}
  \end{block}
\end{frame}