### Nuprl Lemma : previous-event-exists

`∀es:EO. ∀i:Id.`
`  ∀[R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]`
`    ∀e:E`
`      ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)`
`      `` (∃e':E. (e' ≤loc e  c∧ R[e']))`
`         `` (∃e':E. (e' ≤loc e  c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') `` e'' ≤loc e  `` (¬R[e''])))))) `
`         supposing loc(e) = i ∈ Id)`

Proof

Definitions occuring in Statement :  es-le: `e ≤loc 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]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  es-le-self es-locl_transitivity2 es-locl_irreflexivity Id_wf es-loc_wf es-le_wf es-locl_wf es-E_wf es-le-loc all_wf not_wf decidable__assert es-first_wf2 es-le-iff and_wf equal_wf es-pred_wf es-pred-locl es-pred-loc-base iff_weakening_equal es-loc-pred es-le-pred es-locl_transitivity1 es-le_weakening member_wf
\mforall{}es:EO.  \mforall{}i:Id.
\mforall{}[R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
\mforall{}e:E
((\mforall{}e:E.  Dec(R[e])  supposing  loc(e)  =  i)
{}\mRightarrow{}  (\mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  R[e']))
{}\mRightarrow{}  (\mexists{}e':E
(e'  \mleq{}loc  e    c\mwedge{}  (R[e']  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}R[e'']))))))
supposing  loc(e)  =  i)

Date html generated: 2015_07_17-AM-08_50_37
Last ObjectModification: 2015_02_04-PM-05_56_19

Home Index