3/183
\begin{frame}<10>{Reminder: Formula Truth in a Model}
\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}