Nuprl Lemma : es-maximal-event
∀es:EO
∀[P:E ─→ ℙ]
((∀e:E. Dec(P[e]))
⇒ (∀e:E
((∃m:E. (m ≤loc e ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc e ⇒ (¬P[e'])))))
∨ (∀e':E. (e' ≤loc e ⇒ (¬P[e']))))))
Proof
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
function: x:A ─→ B[x]
Lemmas :
or_wf,
exists_wf,
es-E_wf,
es-le_wf,
all_wf,
es-locl_wf,
not_wf,
es-causl_wf,
decidable_wf,
event_ordering_wf,
es-le-self,
es-locl_transitivity2,
es-locl_irreflexivity,
decidable__assert,
es-first_wf2,
es-le-first,
assert_elim,
and_wf,
equal_wf,
bool_wf,
ifthenelse_wf,
es-pred_wf,
es-pred-locl,
es-causl_weakening,
es-locl_transitivity1,
es-le_weakening,
es-le-pred,
es-le-iff
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]
((\mforall{}e:E. Dec(P[e]))
{}\mRightarrow{} (\mforall{}e:E
((\mexists{}m:E. (m \mleq{}loc e \mwedge{} P[m] \mwedge{} (\mforall{}e':E. ((m <loc e') {}\mRightarrow{} e' \mleq{}loc e {}\mRightarrow{} (\mneg{}P[e'])))))
\mvee{} (\mforall{}e':E. (e' \mleq{}loc e {}\mRightarrow{} (\mneg{}P[e']))))))
Date html generated:
2015_07_17-AM-08_40_08
Last ObjectModification:
2015_07_16-AM-10_18_13
Home
Index