Nuprl Lemma : CR-initiator1_wf

[s:SES]. (CR-initiator1{i:l}(s) ∈ Basic1)


Proof




Definitions occuring in Statement :  CR-initiator1: CR-initiator1{i:l}(s) ses-basic-sequence1: Basic1 security-event-structure: SES uall: [x:A]. B[x] member: t ∈ T
Lemmas :  basic-seq-1-1_wf cons_wf protocol-action_wf mk-pa_wf atom-sdata_wf nil_wf Id_wf security-event-structure_wf

Latex:
\mforall{}[s:SES].  (CR-initiator1\{i:l\}(s)  \mmember{}  Basic1)



Date html generated: 2015_07_23-PM-00_20_11
Last ObjectModification: 2015_01_29-AM-01_31_12

Home Index