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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] Re: help to prove my first theorem*From*: Jerry James <james@ittc.ku.edu>*Date*: Tue, 27 Jul 2004 14:28:15 -0500*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20040709105435.40260.qmail@web40005.mail.yahoo.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Gnus/5.1006 (Gnus v5.10.6) XEmacs/21.5 (chayote, linux)

M Raghuram <raghu_megh@yahoo.com> wrote: > 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 Your specification is a bit confused. You are saying, "Give me any bitvector m1. I can then produce an m2 such that, if it so happens that xor(m1,m2) = m1, then m2 is nat2bv(0)." I suspect you really mean one of the following: First: THEORY BEGIN m: VAR nat Th1: THEOREM FORALL (m1, m2: bvec[m]): XOR(m1, m2) = m1 IFF bv2nat(m2) = 0 Th2: THEOREM FORALL (m1: bvec[m]): EXISTS (m2: bvec[m]): XOR(m1, m2) = m1 END First Both of those theorems can be proved with a little effort. Read up on the decompose-equality strategy; you'll need it. Also, by changing your use of nat2bv into a use of bv2nat instead, I've made it possible to use the bv2nat_fill_F and bv2nat_eq0 lemmas from the prelude. See what those two lemmas say and think about how they might be used. Good luck! -- Jerry James http://www.ittc.ku.edu/~james/

**References**:**[PVS-Help] help to prove my first theorem***From:*M Raghuram <raghu_megh@yahoo.com>

- Prev by Date:
**Re: [PVS-Help] PVS on Fedora** - Next by Date:
**[PVS-Help] quotient constructions in PVS** - Prev by thread:
**[PVS-Help] help to prove my first theorem** - Next by thread:
**[PVS-Help] PVS on Fedora** - Index(es):