---

{ [d:SecurityData]. [a:Atom1].
    uiff(d:SecurityData||a;(a  sdata-atoms(d))) }

{ Proof }

---

Definitions occuring in Statement :  sdata-atoms: sdata-atoms(d),  sdata: SecurityData,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  not: A,  l_member: (x  l),  free-from-atom: x:T||a,  atom: Atom$n
Definitions :  member: t  T,  rev_implies: P  Q,  implies: P  Q,  cand: A c B,  not: A,  iff: P  Q,  and: P  Q,  or: P  Q,  prop: ,  false: False,  all: x:A. B[x]
Lemmas :  not_wf,  id-sdata_wf,  sdata_wf,  free-from-atom_wf1,  nil_member,  false_wf,  l_member_wf,  not_functionality_wrt_iff,  cons_member

---

\mforall{}[d:SecurityData].  \mforall{}[a:Atom1].    uiff(d:SecurityData||a;\mneg{}(a  \mmember{}  sdata-atoms(d)))


Date html generated: 2011_08_17-PM-07_10_44
Last ObjectModification: 2011_06_18-PM-12_54_51

Home Index