Nuprl Lemma : ses-flow-has

s:SES. ∀es:EO+(Info). ∀e1,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2)  (e2 has a))


Proof




Definitions occuring in Statement :  ses-flow: ses-flow(s;es;a;e1;e2) event-has: (e has a) ses-info: Info security-event-structure: SES event-ordering+: EO+(Info) es-E: E atom: Atom$n all: x:A. B[x] implies:  Q
Lemmas :  ses-flow-implies event-has_wf es-E_wf event-ordering+_subtype es-le_wf es-causle_wf es-causl_wf sdata_wf eclass-val_wf ses-send_wf assert_elim in-eclass_wf es-interface-subtype_rel2 top_wf subtype_top subtype_base_sq bool_wf bool_subtype_base ses-rcv_wf es-E-interface_wf es-locl_wf ses-decrypted_wf ses-encrypted_wf ses-cipher_wf ses-crypt_wf ses-key-rel_wf ses-decryption-key_wf ses-encryption-key_wf not_wf equal-wf-T-base encryption-key_wf atom1_subtype_base ses-decrypt_wf ses-encrypt_wf event-ordering+_wf ses-info_wf security-event-structure_wf

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  (e2  has  a))



Date html generated: 2015_07_23-PM-00_05_17
Last ObjectModification: 2015_01_29-AM-07_47_54

Home Index