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

the "the" operator



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.

-- 
---------------------------------------------------------------------------
  Mauro Gargano
  University of Saarland, Saarbruecken, DE
  Computer Architecture and Parallel Computing
  building 45, room 320                            mauro@wjp.cs.uni-sb.de
---------------------------------------------------------------------------