Nuprl Lemma : ses-decrypt_wf

[s:SES]. (Decrypt ∈ EClass(SecurityData × Key × Atom1))


Proof




Definitions occuring in Statement :  ses-decrypt: Decrypt ses-info: Info security-event-structure: SES encryption-key: Key sdata: SecurityData eclass: EClass(A[eo; e]) atom: Atom$n uall: [x:A]. B[x] member: t ∈ T product: x:A × B[x]
Lemmas :  eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf sdata_wf encryption-key_wf Id_wf bool_wf top_wf

Latex:
\mforall{}[s:SES].  (Decrypt  \mmember{}  EClass(SecurityData  \mtimes{}  Key  \mtimes{}  Atom1))



Date html generated: 2015_07_23-PM-00_03_26
Last ObjectModification: 2015_01_29-AM-07_46_39

Home Index