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

forall clause within a set-comprehension



Is it possible to prove this lemma:

  empty_dict: LEMMA {w: Word |
               FORALL (l: Letter
                       | member(l, dom(LAMBDA (l: Letter): empty))),
               (w1: Word | member(w1, retrDictd(empty))):
                 w = cons(l, w1)}
           =emptyset[Word]

I tried to do a (expand "emptyset"),(apply-extensionality) which leads
me to this state:

{-1}    FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter): empty))),
      (w1: Word | member(w1, retrDictd(empty))):
        x!1 = cons(l, w1)
  |-------
[1]    (({w: Word |
          FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter):
empty))),
          (w1: Word | member(w1, retrDictd(empty))):
            w = cons(l, w1)})
           = ({x: Word | FALSE}))
How can I deal with the FORALL clause within the set comprehension ??

Thanks
-- 
---------------------------------------------------------
 ("\''/").__..-''"`-. .         Gernot Lepuschitz
 `9_ 9  )   `-. (    ).`-._.`)gernot@sbox.tu-graz.ac.at 
 (_Y_.)' ._   ) `._`.  " -.-'   Telematik - Student
 ..`-'_..-_/ /-'_.'/               TU - Graz
(l)-'' ((i).' ((!.'              
In the softwarerequirements they said Win95 or better
so I installed Linux.