---

{ d:SecurityData. a:Atom1.  (d:SecurityData||a  (a  sdata-atoms(d))) }

{ Proof }

---

Definitions occuring in Statement :  sdata-atoms: sdata-atoms(d),  sdata: SecurityData,  all: x:A. B[x],  iff: P  Q,  not: A,  l_member: (x  l),  free-from-atom: x:T||a,  atom: Atom$n
Definitions :  all: x:A. B[x],  member: t  T,  iff: P  Q,  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  not: A,  decidable: Dec(P),  or: P  Q,  false: False,  prop:
Lemmas :  sdata-free-from-atom,  sdata_wf,  not_wf,  free-from-atom_wf1,  l_member_wf,  sdata-atoms_wf,  decidable__l_member,  decidable__atom_equal_1

---

\mforall{}d:SecurityData.  \mforall{}a:Atom1.    (\mneg{}d:SecurityData||a  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d)))


Date html generated: 2010_08_28-AM-01_49_14
Last ObjectModification: 2009_12_17-PM-10_12_52

Home Index