Nuprl Lemma : CR-responder1_wf

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


Proof




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

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



Date html generated: 2015_07_23-PM-00_20_25
Last ObjectModification: 2015_01_29-AM-01_31_07

Home Index