---

{ [s:SES]. [pas:Id  Id  Atom1  (ProtocolAction List)].
    (A  B: pas[A;B;m]  Basic1) }

{ Proof }

---

Definitions occuring in Statement :  basic-seq-1-1: A  B: pas[A; B; m],  ses-basic-sequence1: Basic1,  protocol-action: ProtocolAction,  security-event-structure: SES,  Id: Id,  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3],  member: t  T,  function: x:A  B[x],  list: type List,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  member: t  T,  ses-basic-sequence1: Basic1,  basic-seq-1-1: A  B: pas[A; B; m],  so_apply: x[s1;s2;s3],  exists: x:A. B[x],  prop:
Lemmas :  ses-is-protocol-actions_wf,  ses-thread_wf,  event-ordering+_wf,  ses-info_wf,  Id_wf,  protocol-action_wf,  security-event-structure_wf

---

\mforall{}[s:SES].  \mforall{}[pas:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  (ProtocolAction  List)].    (A  {}\mrightarrow{}  B:  pas[A;B;m]  \mmember{}  Basic1)


Date html generated: 2011_08_17-PM-07_42_08
Last ObjectModification: 2011_06_18-PM-01_35_58

Home Index