We presents an approach to reason about specifications written in a formal specification language automatically. Our reasoning approach is based as follows: (1)Specifications are written in Z, one of formal specification languages. (2)Reasoning system is based on W, a logic for the Z notation. (3)Verification system is written using CafeOBJ. The logic W is similar to a sequent calculus in the style of Gentzen. CafeOBJ is an executable algebraic specification language. Therefore our approach attempts to transform the specifications into sequents. This paper gives an example how to translate the Z. notations into sequents and how to prove using them.