\newcommand{\select}{\operatorname{select}}
\newcommand{\store}{\operatorname{store}}

\begin{slide}{Definition}

\begin{itemize}\itemsep 0pt \parskip 2pt
\item Signatur mit Sorten: Array, Index, Element
\item Symbole: Gleichheit, \\
  select : Array $\times$ Index $\to$ Element, \\
  store : Array $\times$ Index $\times$ Element 
  $\to$ Array
\item Axiome:
  $\forall a\in\text{Array},i,j\in\text{Index},
  e\in\text{Element}: 
  \select (\store(a,i,e),j)= \dots$
\end{itemize}
\\
John McCarthy and James Painter:
\emph{Correctness of a Compiler for Arithmetic Expressions}, AMS 1967,
\begin{small}
\url{http://www-formal.stanford.edu/jmc/mcpain.html},
\url{http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2}
\end{small}

\end{slide}

