[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Equivalence through XOR
You need to use (apply-extensionality) on the consequent
and (decompose-equality) on the antecedent, and then (grind)
completes the proof.
> It is shown in the bitvector library that for bitvectors bv1 and bv2 of length
> (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