Nuprl Lemma : ses-flow-axiom_wf

[s:SES]. (PropertyF ∈ ℙ')


Proof




Definitions occuring in Statement :  ses-flow-axiom: PropertyF 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-new_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype top_wf subtype_top event-has_wf eclass-val_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base ses-flow_wf ses-sign_wf sdata_wf Id_wf ses-sig_wf exists_wf ses-encrypt_wf encryption-key_wf ses-crypt_wf security-event-structure_wf

Latex:
\mforall{}[s:SES].  (PropertyF  \mmember{}  \mBbbP{}')



Date html generated: 2015_07_23-PM-00_06_27
Last ObjectModification: 2015_01_29-AM-07_48_55

Home Index