 Denney, Fischer &amp; Schumann 2004 describe a system to automate the certification of safety properties of data-analysis aerospace software at NASA. Using Hoare-style program verification techniques, their system generates proof obligations that are then handled by an automated theorem prover. The process is not fully automated, however, since many of the obligations must be simplified first in order to improve the ability of the theorem prover to solve the proof tasks. For example, one such class of obligations makes a statement about a matrix, r, that needs to remain symmetric after updates along its diagonal have been made, and has the form: