Definition

(SMTLIB: QF_A)

• Signatur mit Sorten: Array, Index, Element
• Symbole: Gleichheit,
  select : Array × Index $\to$ Element,
  store : Array × Index × Element $\to$ Array
• Axiom: $\forall$a $\in$ Array, i, j $\in$ Index, e $\in$ Element : select(store(a, i, e)) = ...

John McCarthy and James Painter: Correctness of a Compiler for Arithmetic Expressions, AMS 1967, http://www-formal.stanford.edu/jmc/mcpain.html