[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] about PVS ASSUMPTIONS
have you tried to introduce those as axioms for your lemma?
Nikhil D. Kikkeri wrote:
> i am writing a theory about which takes no formal parameters.i have
> declared three variables
> flp: var bvec
> fsopa: var bvec
> seff: var bit.
> my lemmas will work only under the assumption that
> flp(53) = TRUE or flp(52) = TRUE
> fsopa(117) = seff
> fsopa(116) = seff
> if i do not have any formal parameters, PVS complains that i do not
> need an ASSUMING block.whatever the case might be i need to set those
> bits to those values to use it later on.how can I do that.is there a
> different way of stating these assumptions.
> Want to meet David Beckham? http://www.msn.co.in/gillette/ Fly to
> Madrid with Gillette!