A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis, and automated theroem-proving. This paper presents a decision procedure for an extensional theory of arrays and proves it correct.