Re: the "the" operator

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

```