Nuprl Lemma : member-es-before
∀the_es:EO. ∀e',e:E. ((e ∈ before(e')) ⇐⇒ (e <loc e'))
Proof
Definitions occuring in Statement :
es-before: before(e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
l_member: (x ∈ l),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q
Lemmas :
es-first_wf2,
bool_wf,
equal-wf-T-base,
assert_wf,
bnot_wf,
not_wf,
es-first-implies,
member-implies-null-eq-bfalse,
es-E_wf,
nil_wf,
null_nil_lemma,
btrue_wf,
btrue_neq_bfalse,
l_member_wf,
es-locl_wf,
es-pred_wf,
es-pred-locl,
nil_member,
false_wf,
or_wf,
equal_wf,
es-before_wf,
iff_wf,
cons_member,
cons_wf,
member_append,
append_wf,
es-locl-iff
\mforall{}the$_{es}$:EO. \mforall{}e',e:E. ((e \mmember{} before(e')) \mLeftarrow{}{}\mRightarrow{} (e <loc e'))
Date html generated:
2015_07_17-AM-08_40_23
Last ObjectModification:
2015_01_27-PM-02_41_48
Home
Index