Nuprl Lemma : existse-between3_wf

[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| (loc(e) loc(e1) ∈ Id) ∧ (¬↑first(e))}  ─→ ℙ].
  ∃e∈(e1,e2].P[e] ∈ ℙ supposing loc(e2) loc(e1) ∈ Id


Proof




Definitions occuring in Statement :  existse-between3: e∈(e1,e2].P[e] es-first: first(e) es-loc: loc(e) es-E: E event_ordering: EO Id: Id assert: b uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s] not: ¬A and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  exists_wf es-E_wf es-locl_wf es-le_wf es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 Id_wf es-loc_wf not_wf equal_wf
\mforall{}[es:EO].  \mforall{}[e1,e2:E].  \mforall{}[P:\{e:E|  (loc(e)  =  loc(e1))  \mwedge{}  (\mneg{}\muparrow{}first(e))\}    {}\mrightarrow{}  \mBbbP{}].
    \mexists{}e\mmember{}(e1,e2].P[e]  \mmember{}  \mBbbP{}  supposing  loc(e2)  =  loc(e1)



Date html generated: 2015_07_17-AM-08_48_13
Last ObjectModification: 2015_01_27-PM-02_25_56

Home Index