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