Nuprl Lemma : es-first-event_wf
∀[es:EO]. ∀[e:E]. ∀[P:{e':E| e' ≤loc e } ─→ 𝔹].
(es-first-event(es;P;e) ∈ (∃e':{E| (e' ≤loc e ∧ (↑(P e')) ∧ (∀e'':E. ((e'' <loc e') ⇒ (¬↑(P e'')))))})
∨ (↓∀e':E. (e' ≤loc e ⇒ (¬↑(P e')))))
Proof
Definitions occuring in Statement :
es-first-event: es-first-event(es;P;e),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
assert: ↑b,
bool: 𝔹,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x]
Lemmas :
squash_wf,
all_wf,
es-le_wf,
not_wf,
assert_wf,
sq_exists_wf,
es-locl_wf,
es-locl_transitivity2,
es-le_weakening,
or_wf,
exists_wf,
select_wf,
sq_stable__le,
member-es-le-before,
int_seg_subtype-nat,
false_wf,
less_than_wf,
int_seg_wf,
es-le-before_wf2,
less_than_transitivity2,
le_weakening2,
length_wf,
es-E_wf,
Id_wf,
es-loc_wf,
es-le-before_wf,
equal_wf,
lelt_wf,
es-locl_transitivity1,
es-le_weakening_eq,
l_before-es-le-before-iff,
true_wf,
event_ordering_wf,
iff_weakening_equal,
l_before_no_repeats,
subtype_rel_list,
es-le-before-no_repeats,
decidable__lt,
less-iff-le,
add_functionality_wrt_le,
add-swap,
add-commutes,
le-add-cancel,
assert_elim,
not_assert_elim,
btrue_neq_bfalse
\mforall{}[es:EO]. \mforall{}[e:E]. \mforall{}[P:\{e':E| e' \mleq{}loc e \} {}\mrightarrow{} \mBbbB{}].
(es-first-event(es;P;e) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc e
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e'' <loc e') {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mdownarrow{}\mforall{}e':E. (e' \mleq{}loc e {}\mRightarrow{} (\mneg{}\muparrow{}(P e')))))
Date html generated:
2015_07_17-AM-08_44_56
Last ObjectModification:
2015_02_04-AM-07_10_56
Home
Index