\newcommand{\HALFADD}{\operatorname{HALFADD}}
\newcommand{\FULLADD}{\operatorname{FULLADD}}
\newcommand{\xor}{\operatorname{xor}}

\begin{slide}{Binäre Addition}

$[x_0,\ldots] + [y_0,\ldots]  = [z_0,\ldots] $

Hilfsvariablen: $[c_0,\ldots]$ $=$ Überträge

\begin{itemize}
\item Anfang: $\HALFADD(x_0,y_0;z_0,c_0)$
\item Schritt: $\forall i: \FULLADD(x_i,y_i,c_i;z_i,c_{i+1})$
\item Ende: $c_{w} = 0$ (kein Überlauf)
\end{itemize}
Realisierung:
\begin{itemize}
\item $\HALFADD(x,y;z,c) \iff (z \leftrightarrow \xor(x,y))
  \wedge (c \leftrightarrow x\wedge y)$
\item $\FULLADD(x,y,c;z,c') \iff \dots$
  (zweimal $\HALFADD$)  
\end{itemize}
dafür CNF ohne Hilfsvariablen!

\end{slide}
