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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Equivalence through XOR*From*: Nikhil Kikkeri <nikhil@xxxxxxxxxxxx>*Date*: Thu, 12 Oct 2006 14:50:46 -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>*Organization*: SMU*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: KMail/1.5.3

Hi-- It is shown in the bitvector library that for bitvectors bv1 and bv2 of length n (bv1 = bv2) => (bv1 XOR bv2 = fill[n](FALSE)) But the reverse is true as well, (bv1 XOR bv2 = fill[n](FALSE)) => (bv1 = bv2) So it really should be, (bv1 = bv2) IFF (bv1 XOR bv2 = fill[n](FALSE)) because this is how I would check if two strings were equal. So why is proving the reverse turning to be tricky (assuming that I am correct) ? Thank you, Best regards Nikhil -- Every Horse has an Infinite Number of Legs (proof by intimidation): Horses have an even number of legs. Behind they have two legs, and in front they have fore-legs. This makes six legs, which is certainly an odd number of legs for a horse. But the only number that is both even and odd is infinity. Therefore, horses have an infinite number of legs. Now to show this for the general case, suppose that somewhere, there is a horse that has a finite number of legs. But that is a horse of another color, and by the lemma ["All horses are the same color"], that does not exist.

- Prev by Date:
**[PVS-Help] running PVS on windows through exceed** - Next by Date:
**Re: [PVS-Help] Equivalence through XOR** - Prev by thread:
**Re: [PVS-Help] Problem starting up PVS** - Next by thread:
**Re: [PVS-Help] Equivalence through XOR** - Index(es):