LARA This is an old revision of the document! Arrays are Functions A simple theory of arrays is obtained if we simply allow function update expressions in FOL, as in FOL with Update Expressions. Calculus of Computation Textbook Section 9.5 The UCLID Decision Procedure