### Nuprl Lemma : es-first-at-exists-cases

`∀es:EO. ∀e:E.`
`  ∀[P:{e':E| loc(e') = loc(e) ∈ Id}  ─→ ℙ]`
`    ((∀e':{e':E| loc(e') = loc(e) ∈ Id} . Dec(P[e']))`
`    `` ((∀e'≤e.¬P[e'] ∧ (¬∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e']))`
`       ∨ ((¬∀e'≤e.¬P[e']) ∧ ∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e'])))`

Proof

Definitions occuring in Statement :  es-first-at: `e is first@ i s.t.  e.P[e]` alle-le: `∀e≤e'.P[e]` existse-le: `∃e≤e'.P[e]` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  decidable__alle-le Id_wf es-loc_wf not_wf decidable__not equal_wf alle-le_wf existse-le_wf es-first-at_wf es-first-at-exists2 all_wf es-E_wf decidable_wf event_ordering_wf
\mforall{}es:EO.  \mforall{}e:E.
\mforall{}[P:\{e':E|  loc(e')  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
((\mforall{}e':\{e':E|  loc(e')  =  loc(e)\}  .  Dec(P[e']))
{}\mRightarrow{}  ((\mforall{}e'\mleq{}e.\mneg{}P[e']  \mwedge{}  (\mneg{}\mexists{}e'\mleq{}e.e'  is  first@  loc(e)  s.t.    e'.P[e']))
\mvee{}  ((\mneg{}\mforall{}e'\mleq{}e.\mneg{}P[e'])  \mwedge{}  \mexists{}e'\mleq{}e.e'  is  first@  loc(e)  s.t.    e'.P[e'])))

Date html generated: 2015_07_17-AM-08_50_12
Last ObjectModification: 2015_01_27-PM-02_25_41

Home Index