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

*To*: Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>*Subject*: Re: the "the" operator*From*: Sam Owre <owre@csl.sri.com>*Date*: Mon, 03 Feb 2003 14:30:48 -0800*cc*: pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Mon, 03 Feb 2003 22:21:21 +0100." <3E3EDD51.5020503@wjp.cs.uni-sb.de>*Sender*: pvs-help-owner@csl.sri.com

Hi, Bruno is right, of course, but there is a minor point I think is worth noting. I created the following theory singleton_the: THEORY BEGIN k: VAR nat found?: pred[nat] f: FORMULA singleton?({k | found?(k)}) AND found?(k) => k = the({k | found?(k)}) END singleton_the If you simply run (skosimp) (expand "singleton?") (skosimp) (inst-cp -1 "k!1") (inst -1 "the({k | found?(k)})") then this last instantiation will lead to two goals, one of which is that "{k | found?(k)}" is a singleton. This was a hypothesis earlier, but was expanded out and is no longer readily available. The right way to deal with this is to use (assert) before expanding singleton? - that way the hypotheses are recorded, and the second subgoal is no longer generated. Sam > Mauro Gargano wrote: > > Hi again, > > > > It should be easy to prove but I don't know how: > > > > > > [-1] singleton?(LAMBDA (i: subrange(j!1, l`len - 1)): found?(Nth(l, i))) > > [-2] 0 <= j!1 > > [-3] j!1 <= len(l) - 2 > > [-4] j!1 >= 0 > > [-5] j!1 < l`len > > [-6] found?(Nth(l, j!1)) > > |------- > > [1] j!1 = the(LAMBDA (k: subrange(j!1, l`len - 1)): found?(Nth(l, k))) > > > > > > > > I have a predicate true for j!1, I have the hypotesis of uniquenes, > > so the set is "singleton?" and the "the" operator should give back the > > value j!1....am I wrong? > > > > > > > > please, give me a feedback. > > > > Mauro. > > > > Hi, > > Expanding the definition of "singleton?" followed by > (skolem!) and two instantiations should work. > > Bruno > -- > Bruno Dutertre | bruno@sdl.sri.com > SDL, SRI International | fax: 650 859-2844 > 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717 >

**References**:**the "the" operator***From:*Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>

- Prev by Date:
**Re: the "the" operator** - Next by Date:
**intersection, implication, predicate problem, specific exampleproblem** - Prev by thread:
**Re: the "the" operator** - Next by thread:
**reduce_nat( ... )** - Index(es):