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

[PVS-Help] Equivalence through XOR



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.