[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] help to prove my first theorem
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
m : Var nat
Th1 : Theorem Forall (m1: bvec[m]): exists
(m2:bvec[m]): (xor(m1,m2) = m1) => (m2=nat2bv(0))
Do you Yahoo!?
New and Improved Yahoo! Mail - 100MB free storage!