
\newcommand{\wert}{\operatorname{\mathsf{wert}}}
% \newcommand{\BB}{\mathbb{B}}
\newcommand{\ZZ}{\mathbb{Z}}

\begin{slide}{Inferenz von Werten}

  \begin{itemize}
  \item 
Grundbereich: Aussagen der Form $\wert(p,z)$
mit $p \in \texttt{Exp}$ , $z\in \ZZ$

\begin{verbatim}
data Exp = Const Integer
         | Plus Exp Exp
         | Times Exp Exp
\end{verbatim}

\item
Axiome: $\wert(\texttt{Const} z,z)$
\item 
Regeln: 

\( \displaystyle
\frac{\wert(X,a),\wert(Y,b)}
{\wert(\texttt{Plus} ~ X ~ Y,a+b)},
\quad
\frac{\wert(X,a),\wert(Y,b)}
{\wert(\texttt{Times} ~ X ~ Y,a\cdot b)},
\dots
\)
\end{itemize}


\end{slide}

