### Nuprl Lemma : es-first-at-since-iff

`∀es:EO. ∀i:Id. ∀e:E.`
`  ∀[P,R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ].`
`    ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)`
`    `` (es-first-at-since(es;i;e;e.R[e];e.P[e])`
`       `⇐⇒` (loc(e) = i ∈ Id)`
`           c∧ ((P[e] ∧ (¬R[e]))`
`              ∧ ((∃e'':E. ((e'' <loc e) c∧ P[e'']))`
`                `` (∃e':E`
`                     ((e' <loc e)`
`                     c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') `` (e'' <loc e) `` ((¬P[e'']) ∧ (¬R[e''])))))))))))`

Proof

Definitions occuring in Statement :  es-first-at-since: `es-first-at-since(es;i;e;e.R[e];e.P[e])` es-locl: `(e <loc e')` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` cand: `A c∧ B` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  Id_wf es-loc_wf exists_wf es-E_wf es-locl_wf es-first-at-since_wf not_wf all_wf isect_wf decidable_wf event_ordering_wf previous-event-exists es-le_weakening es-le_wf es-le-loc and_wf equal_wf es-locl_transitivity2 es-le-not-locl
\mforall{}es:EO.  \mforall{}i:Id.  \mforall{}e:E.
\mforall{}[P,R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].
((\mforall{}e:E.  Dec(R[e])  supposing  loc(e)  =  i)
{}\mRightarrow{}  (es-first-at-since(es;i;e;e.R[e];e.P[e])
\mLeftarrow{}{}\mRightarrow{}  (loc(e)  =  i)
c\mwedge{}  ((P[e]  \mwedge{}  (\mneg{}R[e]))
\mwedge{}  ((\mexists{}e'':E.  ((e''  <loc  e)  c\mwedge{}  P[e'']))
{}\mRightarrow{}  (\mexists{}e':E
((e'  <loc  e)
c\mwedge{}  (R[e']
\mwedge{}  (\mforall{}e'':E
((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  ((\mneg{}P[e''])  \mwedge{}  (\mneg{}R[e''])))))))))))

Date html generated: 2015_07_17-AM-09_05_40
Last ObjectModification: 2015_01_27-PM-00_49_44

Home Index