---

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

{ Proof }

---

Definitions occuring in Statement :  basic-seq-1-4: A  B: pas[A;B;m;n;x;y],  ses-basic-sequence1: Basic1,  protocol-action: ProtocolAction,  security-event-structure: SES,  Id: Id,  uall: [x:A]. B[x],  so_apply: x[a;b;c;d;e;f],  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-4: A  B: pas[A;B;m;n;x;y],  so_apply: x[a;b;c;d;e;f],  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{}  Atom1  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  (ProtocolAction  List)].
    (A  {}\mrightarrow{}  B:  pas[A;B;m;n;x;y]  \mmember{}  Basic1)


Date html generated: 2011_08_17-PM-07_42_42
Last ObjectModification: 2011_06_18-PM-01_36_54

Home Index