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
Lemmas :  set_wf assert_wf subtype_base_sq equal-wf-base equal-wf-base-T equal-wf-T-base squash_wf true_wf false_wf existse-between1_wf Id_wf es-loc_wf es-E_wf event_ordering_wf
\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: 2015_07_17-AM-08_47_27
Last ObjectModification: 2015_01_27-PM-02_25_29

Home Index