Nuprl Lemma : es-last-event_wf
∀[es:EO]. ∀[e:E]. ∀[P:{e':E| e' ≤loc e } ─→ 𝔹].
(es-last-event(es;P;e) ∈ (∃e':{E| (e' ≤loc e ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc e ∧ (↑(P e')))})))
Proof
Definitions occuring in Statement :
es-last-event: es-last-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,
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 :
es-first_wf2,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
it_wf,
not_assert_elim,
es-le-self,
es-le_wf,
es-le-first,
assert_elim,
and_wf,
ifthenelse_wf,
es-E_wf,
btrue_neq_bfalse,
sq_exists_wf,
assert_wf,
all_wf,
es-locl_wf,
not_wf,
es-pred_wf,
es-pred-locl,
es-causl_weakening,
subtype_rel_dep_function,
subtype_rel_sets,
es-locl_transitivity1,
es-le_weakening,
subtype_rel_self,
set_wf,
es-pred_property,
or_wf,
es-le-pred,
es-le_weakening_eq,
subtype_rel_not
\mforall{}[es:EO]. \mforall{}[e:E]. \mforall{}[P:\{e':E| e' \mleq{}loc e \} {}\mrightarrow{} \mBbbB{}].
(es-last-event(es;P;e) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc e
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc e {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc e \mwedge{} (\muparrow{}(P e')))\})))
Date html generated:
2015_07_17-AM-08_39_32
Last ObjectModification:
2015_01_27-PM-02_43_57
Home
Index