Re: [PVS-Help] Equivalence through XOR

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

Nikhil:
   You need to use (apply-extensionality) on the consequent
and (decompose-equality) on the antecedent, and then (grind)
completes the proof.

-Shankar

> 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