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

*To*: pvs-help@csl.sri.com*Subject*: can you give me command to prove test??*From*: chao qin <Chao.Qin@loria.fr>*Date*: Sat, 05 Jul 2003 17:32:26 +0200*Organization*: loria*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3.1) Gecko/20030425

Hi,everyone: I am just new beginner in PVS, I found the example in maillist ,but I cann't prove it,after I used (grind) command, it need to prove : test : {-1} b!1(x!1) |------- {1} a!1(x!1) I don't know how to do it,can you give me some advice. the follow is the example given by John foo[T: TYPE]:THEORY BEGIN set1: TYPE = finite_set[T] set2: TYPE = {t: finite_set[T]| FORALL (s:set1): subset?(t,s)} a: VAR set1 b: VAR set2 test: LEMMA subset?(b,a) END foo You can then prove test from the type predicate on b. best regards

- Prev by Date:
**License as ASCII text?** - Next by Date:
**Re: can you give me command to prove test??** - Prev by thread:
**Re: pb with measure in a recursive function** - Next by thread:
**Re: can you give me command to prove test??** - Index(es):