High Performance Deduction for verification: a case study in the theory of arrays