Nuprl Lemma : basic-seq-1-4_wf

[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 list: List atom: Atom$n uall: [x:A]. B[x] so_apply: x[a;b;c;d;e;f] member: t ∈ T function: x:A ─→ B[x]
Lemmas :  exists_wf ses-is-protocol-actions_wf ses-thread_wf event-ordering+_wf ses-info_wf Id_wf list_wf protocol-action_wf security-event-structure_wf

Latex:
\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: 2015_07_23-PM-00_16_28
Last ObjectModification: 2015_01_29-AM-01_31_58

Home Index