Hi, Isn't it possible to use one of the lemmas (which has been already proved) in the specification to prove one of the TCCS? Thanks, Borzoo ------------------------------------------------------------------------ Borzoo Bonakdarpour Graduate Research Assistant Department of Computer Science & Engineering Michigan State University E-mail: borzoo@cse.msu.edu URL: http://www.cse.msu.edu/~borzoo