Nuprl Lemma : alle-between1-true

[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) loc(e1) ∈ Id} ].  uiff(∀e∈[e1,e2).True;True)


Proof




Definitions occuring in Statement :  alle-between1: e∈[e1,e2).P[e] es-loc: loc(e) es-E: E event_ordering: EO Id: Id uiff: uiff(P;Q) uall: [x:A]. B[x] true: True set: {x:A| B[x]}  equal: t ∈ T
Lemmas :  alle-between1_wf Id_wf es-loc_wf es-locl_wf es-le_wf set_wf es-E_wf true_wf
\mforall{}[es:EO].  \mforall{}[e1:E].  \mforall{}[e2:\{e:E|  loc(e)  =  loc(e1)\}  ].    uiff(\mforall{}e\mmember{}[e1,e2).True;True)



Date html generated: 2015_07_17-AM-08_47_07
Last ObjectModification: 2015_01_27-PM-02_26_27

Home Index