Sometimes people consider theory of arrays. A simple theory of arrays is obtained if we simply allow function update expressions in FOL, as in FOL with Update Expressions.