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

[PVS-Help] Problems in proving a lemma


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 

         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 

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.


Marriage? Join BharatMatrimony.com for free.