Nuprl Lemma : existse-between1-false

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


Proof




Definitions occuring in Statement :  existse-between1: e∈[e1,e2).P[e] es-loc: loc(e) es-E: E event_ordering: EO Id: Id all: x:A. B[x] iff: ⇐⇒ Q false: False 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 false: False existse-between1: e∈[e1,e2).P[e] exists: x:A. B[x] cand: c∧ B

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



Date html generated: 2016_05_16-AM-09_44_04
Last ObjectModification: 2015_12_28-PM-09_39_30

Theory : new!event-ordering


Home Index