### 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