hi-- is there a lemma already defined in PVS that shows (1-a)(1+a) = (1-a^2) if not,how do i go about it thank you -Nikhil --- http://engr.smu.edu/~nikhil _________________________________________________________________ Expressions unlimited! http://server1.msn.co.in/sp04/messenger/ The all new MSN Messenger!