[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?
http://creative.mediaturf.net/creatives/timesjobs/hotmail_TOL.htm Log on to
timesjobs.com and apply TODAY!