[PVS-Help] Regarding "replace", "name-replace" w.r.t bv2int

```Hi--

I don't know whether the following is a bug or just a quirk of using bv2int.

The problem is as follows. I have something like
bv2int(w(x(y(z(arg1,arg2)))))*2^-116 about which I need to prove a certain
property. The expressions w,x,y,z when used in the fashion shown above
result in a bitvector of length 118. There are ways to simplify the
expressions within bv2int which results in

bv2int(fill[63](TRUE) o bv) *2^-116 where bv is of length 55. Next what I
want to do is to transform it to

bv2int(fill[63](TRUE) o bv)*2^(63 - (d-1))*2^-116 + (2^(63 - (d - 1)) -
1)*2^-116 and then

subsequently getting it to the form

(2*bv2int(fill[63](TRUE) o bv + 1)*2^-d)/2^53 - 2^-116. Of course, the above
is true only when

(d-1) = 63.

I have a few lemmas that should allow me to do the replacements. However, I
noticed that for some reason I am not able to rewrite any of the terms
involving bv2int in the consequent. I can rewrite the same term in the
antecedent though. In fact even name-replace does not work for the bv2int
expression in the consequent. However, also, I noticed that name-replace
works in the early stages of the proof (namely when most of the expressions
have not been expanded and rewritten). Same applies for replace as well.

I have checked my specifications for any inconsistencies that might prevent
the rewrites but they appear to be clean.

Any suggestions on why something like this might occur and how can I work
around it? I am using PVS 3.2

Thank you,

rgds
-Nikhil

---
http://engr.smu.edu/~nikhil

```