[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Bitvector concatanation
I am having problems in proving a lemma that says
for a bitvector bv:bvec[n+1]
bv2nat(bv(n) o NOT bv(n))*2^n + bv2nat(bv^(n-1,0)) = bv2nat(bv(n) o NOT
bv(n) o bv^(n-1,0))
bv2nat_concat does not work. What i would like to do is split the second
concatanation on the right side which will make LHS = RHS.
Alternatively I would like to split off the two bits on the right hand side
thus getting rid of the concatanation.
http://www.bharatmatrimony.com/cgi-bin/bmclicks1.cgi?72 Unmarried? Join