Definition

• Signatur mit Sorten: Array, Index, Element
• Symbole: Gleichheit,
  select : Array × mathend000# Index → mathend000# Element,
  store : Array × mathend000# Index × mathend000# Element → mathend000# Array
• Axiome: ∀a∈Array, i, j∈Index, e∈Element : select(store(a, i, e), j) = ... mathend000#

John McCarthy and James Painter: Correctness of a Compiler for Arithmetic Expressions, AMS 1967, http://www-formal.stanford.edu/jmc/mcpain.html, http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2