Nuprl Lemma : ses-nonce-from-ordering
∀s:SES. (ActionsDisjoint ⇒ PropertyO ⇒ PropertyN)
Proof
Definitions occuring in Statement :
ses-disjoint: ActionsDisjoint,
ses-nonce: PropertyN,
ses-ordering: PropertyO,
security-event-structure: SES,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
ses-ordering-ordering',
ses-ordering_wf,
ses-disjoint_wf,
security-event-structure_wf,
event-has*_wf,
eclass-val_wf,
es-E_wf,
event-ordering+_subtype,
ses-new_wf,
assert_elim,
in-eclass_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
es-E-interface_wf,
es-interface-subtype_rel2,
top_wf,
subtype_top,
event-ordering+_wf,
ses-info_wf,
es-causle_weakening_locl,
es-le-loc,
not_wf,
equal_wf,
Id_wf,
es-loc_wf,
es-causl_transitivity2,
es-causl_weakening,
es-causle_weakening,
es-locl_wf,
es-causl_wf
Latex:
\mforall{}s:SES. (ActionsDisjoint {}\mRightarrow{} PropertyO {}\mRightarrow{} PropertyN)
Date html generated:
2015_07_23-PM-00_08_53
Last ObjectModification:
2015_01_29-AM-07_51_03
Home
Index