\begin{slide}{Spezialfälle}

durch beschriebene Transformation
kann man Array-Logik reduzieren
auf Kombination von 
\begin{itemize}
\item Index-Logik (z. B. lineare Arithmetik)
\item Element-Logik 
\item uninterpretierte Funktionen.
\end{itemize}
Lösen mit Nelson-Oppen möglich.

Ähnliche Rechnungen finden (seit vielen Jahrzehnten!)
im Schleifen-Optimiere von \verb|gcc| statt
(Beispiel).

Mit Array-Logik kann man beweisen, 
daß der Optimierer recht hat.

\end{slide}
