Nuprl Lemma : ses-D-private_wf

[s:SES]. (ses-D-private(s) ∈ ℙ')


Proof




Definitions occuring in Statement :  ses-D-private: ses-D-private(s) security-event-structure: SES uall: [x:A]. B[x] prop: member: t ∈ T
Lemmas :  all_wf event-ordering+_wf ses-info_wf es-E-interface_wf ses-decrypt_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype top_wf subtype_top sdata_wf encryption-key_wf Id_wf eclass-val_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base ses-private-key_wf exists_wf ses-encrypt_wf es-causl_wf ses-public-key_wf security-event-structure_wf

Latex:
\mforall{}[s:SES].  (ses-D-private(s)  \mmember{}  \mBbbP{}')



Date html generated: 2015_07_23-PM-00_08_19
Last ObjectModification: 2015_01_29-AM-07_50_16

Home Index