One of the advantages of XYZ/E is that both high level and low level specifications can be represented in the same frame work, so that it makes specification and implementation of software systems easier. It is important to develop verification tools to verify whether the expected relation between different levels of specifications holds. Rules for verification of XYZ/SE programs had been studied by Xie Hongliang et al. in a previous paper. This paper extends the set of the rules to include rules for use of arrays, for procedure specification and for procedure call. It puts the emphasis on the practical and mechanical aspects of the verification of XYZ/SE programs. A set of rules for simplifying verification conditions is also implemented.