Nuprl Lemma : ses-verify-sig_wf

[s:SES]. ∀[es:EO+(Info)]. ∀[e:E(Verify)].  (signature(e) ∈ Atom1)


Proof




Definitions occuring in Statement :  ses-verify-sig: signature(e) ses-verify: Verify ses-info: Info security-event-structure: SES es-E-interface: E(X) event-ordering+: EO+(Info) atom: Atom$n uall: [x:A]. B[x] member: t ∈ T
Lemmas :  eclass-val_wf sdata_wf Id_wf es-E_wf event-ordering+_subtype ses-verify_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(Verify)].    (signature(e)  \mmember{}  Atom1)



Date html generated: 2015_07_23-PM-00_03_03
Last ObjectModification: 2015_01_29-AM-07_45_58

Home Index