Nuprl Lemma : l_before-es-before
∀the_es:EO. ∀e,e',y:E. (e' before y ∈ before(e) ⇒ (e' <loc y))
Proof
Definitions occuring in Statement :
es-before: before(e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
l_before: x before y ∈ l,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
false_wf,
es-E_wf,
nil_before,
l_before_wf,
nil_wf,
all_wf,
decidable__es-E-equal,
es-pred_wf,
append_wf,
es-before_wf,
cons_wf,
member-es-before,
length_of_cons_lemma,
length_of_nil_lemma,
subtype_rel_dep_function,
int_seg_wf,
subtype_rel-int_seg,
length_wf,
length_nil,
non_neg_length,
length_wf_nil,
length_wf_nat,
length_cons,
length_append,
subtype_rel_list,
top_wf,
increasing_wf,
equal_wf,
select_wf,
select_append_front,
iff_weakening_equal,
int_seg_subtype-nat,
less_than_wf,
es-pred-locl,
or_false_r,
or_wf,
not_wf,
nil_member,
l_member_wf,
cons_member,
l_before_append_front
\mforall{}the$_{es}$:EO. \mforall{}e,e',y:E. (e' before y \mmember{} before(e) {}\mRightarrow{} (e' <loc y))
Date html generated:
2015_07_17-AM-08_40_28
Last ObjectModification:
2015_02_04-AM-07_08_36
Home
Index