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

Re: the "the" operator



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