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

[PVS-Help] regarding bv_unary_minus


This lemma is defined in bv_arithmetic of the bitvector library as

bv_unary_minus: LEMMA (-bv) = (NOT bv) + 1

I need to use this lemma in a slightly different form i.e

(NOT bv) = -bv - 1

i went ahead and wrote bv_unary_minus2

bv_unary_minus2:LEMMA (NOT bv) = -bv - 1

while proving I rewrite bv_unary_minus which gives me

(NOT bv!1) = (NOT bv!1) + 1 - 1

However (assert) wont work and consequently the whole thing doesnt work out 
the way I expect.

what am i doing wrong?

Is there a different way to show the same? i.e by rewriting bv2int_inj?




Top-of-the-line jobs!. 
http://creative.mediaturf.net/creatives/timesjobs/hotmail_TOL.htm Log on to 
timesjobs.com and apply TODAY!