Nuprl Lemma : es-pred-exists-between2

`∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) `` (∃e:{e:E| ¬↑first(e)} . ((e1 = pred(e) ∈ E) ∧ e ≤loc e2 )))`

Proof

Definitions occuring in Statement :  es-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-first: `first(e)` es-pred: `pred(e)` es-E: `E` event_ordering: `EO` assert: `↑b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` equal: `s = t ∈ T`
Lemmas :  es-pred-exists-between es-pred_property assert_elim es-first_wf2 es-locl-first btrue_neq_bfalse assert_wf es-causl_weakening es-pred_wf not_assert_elim es-le_wf es-locl_wf es-E_wf event_ordering_wf equal_wf es-pred-one-one es-le-self and_wf es-causl_wf es-loc_wf es-loc-pred es-pred-locl-implies-le es-pred-locl es-locl_transitivity1 es-le_weakening
\mforall{}es:EO.  \mforall{}e1,e2:E.    ((e1  <loc  e2)  {}\mRightarrow{}  (\mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  ((e1  =  pred(e))  \mwedge{}  e  \mleq{}loc  e2  )))

Date html generated: 2015_07_17-AM-08_39_20
Last ObjectModification: 2015_01_27-PM-02_42_20

Home Index