\begin{slide}{Übung Array-Formeln/NNF}

\begin{itemize}\itemsep 0pt
  \item $P\to Q$ in NNF?
  \item $\neg \forall i: P(i) \Rightarrow Q(i)$
    auf \emph{Pränexform} bringen (Quantor(en) außen)
  \item Regel
    \glqq ersetze $\neg\forall i:\dots$ \grqq\
    ist nur korrekt für NNF (Gegenbeispiel?)
  \end{itemize}
Sind die folgenden Eigenschaften durch
Array-Formeln beschreibbar?
  \begin{itemize}\itemsep 0pt
  \item das Array $a$ ist monoton steigend
\item $b$ enthält wenigstens zwei
  verschiedene Einträge
\item für jedes Element $=x$ gibt
  es rechts davon ein Element $\neq x$
\end{itemize}


\end{slide}
