---

{ [s:SES]. (New  EClass(Atom1)) }

{ Proof }

---

Definitions occuring in Statement :  ses-new: New,  ses-info: Info,  security-event-structure: SES,  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  member: t  T,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  member: t  T,  ses-info: Info,  ses-new: New,  pi1: fst(t),  pi2: snd(t),  security-event-structure: SES
Lemmas :  security-event-structure_wf

---

\mforall{}[s:SES].  (New  \mmember{}  EClass(Atom1))


Date html generated: 2011_08_17-PM-07_11_52
Last ObjectModification: 2011_06_18-PM-12_57_51

Home Index