[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 
   structured properly.
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 prove

  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))