Nuprl Lemma : es-before-partition
∀[es:EO]. ∀[e,e':E]. before(e) = (≤loc(e') @ (e', e)) ∈ (E List) supposing (e' <loc e)
Proof
Definitions occuring in Statement :
es-open-interval: (e, e'),
es-le-before: ≤loc(e),
es-before: before(e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
append: as @ bs,
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
es-le-before-partition,
es-le_weakening,
es-locl_wf,
es-E_wf,
event_ordering_wf,
list_wf,
es-before_wf,
append_wf,
es-bless_wf,
bool_wf,
eqtt_to_assert,
assert-es-bless,
cons_wf,
nil_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
es-open-interval_wf,
decidable__equal_int,
length_wf,
false_wf,
not-equal-2,
or_wf,
member_wf,
iff_imp_equal_bool,
btrue_wf,
true_wf,
assert_wf,
iff_wf,
append_assoc_sq,
squash_wf,
es-interval-open-interval,
iff_weakening_equal,
general-append-cancellation
\mforall{}[es:EO]. \mforall{}[e,e':E]. before(e) = (\mleq{}loc(e') @ (e', e)) supposing (e' <loc e)
Date html generated:
2015_07_17-AM-08_43_22
Last ObjectModification:
2015_02_04-AM-07_08_50
Home
Index