# [PVS-Help] regarding properties of floor and ceiling

```Hi--

This is a long e-mail. I am dealing with the following problem

consider the following bitvector of length  6

101011  -> x

If i divide this bitvector by 2^5 = 32 I have a real number equal to 1.34375

Assume that I chop of the bitvector as shown

11  -> the tail

this chopping off is nothing but taking the floor of the real number
above. If the leftmost bit has weight 2^0 then the rightmost bit has
weight 2^-k  (here k = 5)

so if I want a bitvector of precision 3 then I simply say
2^-3*floor(x*2^-5*2^3)   where x is the original bitvector which is
nothing but the head and its value works out to 1.25. the tail works out
to be 0.9375 which is nothing but
2^-P*fractional(x*2^-k*2^P) . so what I have is

x*2^-k = 2^-P*floor(x*2^-k+P) + 2^-P*fractional(x*2^-k+P)

Also at all times P is strictly lesser than k

Now if I move away from bitvectors to a general case for any real number
of the type  y*2^-k where y is of type natural then I face a problem in
proving some essential properties that can be easily shown with
bitvectors. For example I should be able to prove

2^-P*fractional(x*2^-k+P)  <= 2^-P - 2^-k   which in terms of bv is the
maximum value of a bitvector

it can be easily shown that 2^-P*fractional(x*2^-k+P)  < 2^-P  by the
properties of floor in the prelude but the above property is more strict
and relates fractionals with bitvectors. Also it would be nice to show
that if

2^-P*fractional(x*2^-k+P)  /=0 Then

2^-P*fractional(x*2^-k+P)   >= 2^-k

the only thing I have done so far is used the floor and ceiling
definitions and floor_within_1 and floor_0 lemmas to see how far I can
go, but it just keeps me going through circles.

Any clues to solve this would be of great help.

Thank you

rgds
-nikhil

```