---

{ [s:SES]. [bs:Basic1]. [A,B:Id]. [es:EO+(Info)]. [thr:Thread].
    (thr[A;B] |= bs  ) }

{ Proof }

---

Definitions occuring in Statement :  is-basic-seq: thr[A;B] |= bs,  ses-basic-sequence1: Basic1,  ses-thread: Thread,  ses-info: Info,  security-event-structure: SES,  event-ordering+: EO+(Info),  Id: Id,  uall: [x:A]. B[x],  prop: ,  member: t  T
Definitions :  uall: [x:A]. B[x],  ses-basic-sequence1: Basic1,  member: t  T,  is-basic-seq: thr[A;B] |= bs,  prop:
Lemmas :  ses-thread_wf,  event-ordering+_wf,  ses-info_wf,  Id_wf,  ses-basic-sequence1_wf,  security-event-structure_wf

---

\mforall{}[s:SES].  \mforall{}[bs:Basic1].  \mforall{}[A,B:Id].  \mforall{}[es:EO+(Info)].  \mforall{}[thr:Thread].    (thr[A;B]  |=  bs  \mmember{}  \mBbbP{})


Date html generated: 2011_08_17-PM-07_41_47
Last ObjectModification: 2011_06_18-PM-01_35_20

Home Index