---

{ [s:SES]. (Basic1  ') }

{ Proof }

---

Definitions occuring in Statement :  ses-basic-sequence1: Basic1,  security-event-structure: SES,  uall: [x:A]. B[x],  prop: ,  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  ses-basic-sequence1: Basic1
Lemmas :  Id_wf,  event-ordering+_wf,  ses-info_wf,  ses-thread_wf,  security-event-structure_wf

---

\mforall{}[s:SES].  (Basic1  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_17-PM-07_41_36
Last ObjectModification: 2011_06_18-PM-01_35_02

Home Index