[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Problems in proving a lemma
I had sent out a mail yesterday, I guess the mail probably was not
It helps (at least for me) if you attach correct PVS code (or a
dump file) to your message. It takes a lot of time to extract the
problem from an email an retype it in PVS.
This is very obvious but i cant get PVS to see this though.
i, k : Var nat
a : lemma i/exp2(k+1) < exp2(k-0+2)/exp2(k+1) IMPLIES i/exp2(k+1) < 2
;;; Proof a-1 for formula A.a
;;; developed with shostak decision procedures
("" (skosimp* :preds? t) (expand "exp2" -3 2) (assert))