Nuprl Lemma : existse-between2-true

es:EO. ∀e1:E. ∀e2:{e:E| loc(e) loc(e1) ∈ Id} .  (∃e∈[e1,e2].True ⇐⇒ e1 ≤loc e2 )


Proof




Definitions occuring in Statement :  existse-between2: e∈[e1,e2].P[e] es-le: e ≤loc e'  es-loc: loc(e) es-E: E event_ordering: EO Id: Id all: x:A. B[x] iff: ⇐⇒ Q true: True set: {x:A| B[x]}  equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a rev_implies:  Q existse-between2: e∈[e1,e2].P[e] exists: x:A. B[x] cand: c∧ B trans: Trans(T;x,y.E[x; y]) true: True

Latex:
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .    (\mexists{}e\mmember{}[e1,e2].True  \mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2  )



Date html generated: 2016_05_16-AM-09_45_19
Last ObjectModification: 2015_12_28-PM-09_38_42

Theory : new!event-ordering


Home Index