Nuprl Lemma : CR-responder5_wf

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


Proof




Definitions occuring in Statement :  CR-responder5: CR-responder5{i:l}(s) ses-basic-sequence1: Basic1 security-event-structure: SES uall: [x:A]. B[x] member: t ∈ T
Lemmas :  list_ind_cons_lemma list_ind_nil_lemma basic-seq-1-5_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-responder5\{i:l\}(s)  \mmember{}  Basic1)



Date html generated: 2015_07_23-PM-00_24_11
Last ObjectModification: 2015_01_29-AM-01_30_15

Home Index