[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [PVS-Help] Problems in proving a lemma

```
Hello--

I had sent out a mail yesterday, I guess the mail probably was not
structured properly.

Ok, here is what i have done

I have a lemma that proves that a certain quantity is "i" is less than
exp2(u-l+2)

i < exp2(u-l+2)

where u and l are the upper and lower bounds respectively. I have this
proved in PVS

I have another lemma that says  that the same quantity "i" --

i/exp2(k+1) < exp2(k-0+2)/exp2(k+1)     k=upper-bound  0=lower-bound

that is, "i" divided both sides by exp2(k+1)

Effectively what i want to do is show that the left-hand-side is less than
2.

i.e i/exp2(k+1) < 2

This is very obvious but i cant get PVS to see this though.What do i need to
do to make PVS see this.

I will be very happy to mail the theory if someone needs it.

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

_________________________________________________________________
Marriage? Join BharatMatrimony.com for free.
http://www.bharatmatrimony.com/cgi-bin/bmclicks1.cgi?74

```