### Nuprl Lemma : es-minimal-event

`∀es:EO`
`  ∀[P:E ─→ ℙ]. ((∀e:E. Dec(P[e])) `` (∀e:E. (P[e] `` (∃m:E. (m ≤loc e  ∧ P[m] ∧ (∀e':E. ((e' <loc m) `` (¬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` and: `P ∧ Q` function: `x:A ─→ B[x]`
Lemmas :  exists_wf es-E_wf es-le_wf all_wf es-locl_wf not_wf es-causl_wf decidable_wf event_ordering_wf decidable__existse-before subtype_rel_dep_function Id_wf es-loc_wf subtype_rel_self set_wf equal_wf es-causl_weakening es-locl_transitivity1 es-le_weakening es-le-self
\mforall{}es:EO
\mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}]
((\mforall{}e:E.  Dec(P[e]))
{}\mRightarrow{}  (\mforall{}e:E.  (P[e]  {}\mRightarrow{}  (\mexists{}m:E.  (m  \mleq{}loc  e    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((e'  <loc  m)  {}\mRightarrow{}  (\mneg{}P[e']))))))))

Date html generated: 2015_07_17-AM-08_46_03
Last ObjectModification: 2015_01_27-PM-02_28_30

Home Index