Nuprl Lemma : ses-signed_wf

[s:SES]. ∀[es:EO+(Info)]. ∀[e:E(Sign)].  (signed(e) ∈ SecurityData)


Proof




Definitions occuring in Statement :  ses-signed: signed(e) ses-sign: Sign ses-info: Info security-event-structure: SES sdata: SecurityData es-E-interface: E(X) event-ordering+: EO+(Info) uall: [x:A]. B[x] member: t ∈ T
Lemmas :  eclass-val_wf sdata_wf Id_wf es-E_wf event-ordering+_subtype ses-sign_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base es-E-interface_wf ses-info_wf es-interface-subtype_rel2 event-ordering+_wf top_wf subtype_top security-event-structure_wf

Latex:
\mforall{}[s:SES].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E(Sign)].    (signed(e)  \mmember{}  SecurityData)



Date html generated: 2015_07_23-PM-00_02_42
Last ObjectModification: 2015_01_29-AM-07_44_57

Home Index