Nuprl Lemma : basic-seq-1-3_wf

[s:SES]. ∀[pas:Id ─→ Id ─→ Atom1 ─→ Atom1 ─→ Atom1 ─→ (ProtocolAction List)].  (A ─→ B: pas[A;B;m;n;x] ∈ Basic1)


Proof




Definitions occuring in Statement :  basic-seq-1-3: A ─→ B: pas[A; B; m; n; x] 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[s1;s2;s3;s4;s5] 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{}  (ProtocolAction  List)].
    (A  {}\mrightarrow{}  B:  pas[A;B;m;n;x]  \mmember{}  Basic1)



Date html generated: 2015_07_23-PM-00_16_17
Last ObjectModification: 2015_01_29-AM-01_32_06

Home Index