[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] help to prove my first theorem



Hello All,

     I am new to PVS. I wrote my first theorem and I
am not able to prove it using PVS. I have read the
documentation abt the prover but I am not able to do
it. May be its trivial but not yet for me. The
following is my first theory.

First : Theory

Begin
   m : Var nat

Th1 : Theorem Forall (m1: bvec[m]): exists
(m2:bvec[m]): (xor(m1,m2) = m1) => (m2=nat2bv(0))

End First

Thanx,


	
		
__________________________________
Do you Yahoo!?
New and Improved Yahoo! Mail - 100MB free storage!
http://promotions.yahoo.com/new_mail