[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.



Join BharatMatrimony.com. 
http://www.bharatmatrimony.com/cgi-bin/bmclicks1.cgi?72 Unmarried? Join