Nuprl Lemma : es-le-antisymmetric

[es:EO]. ∀[e,e':E].  (e e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )


Proof




Definitions occuring in Statement :  es-le: e ≤loc e'  es-E: E event_ordering: EO uimplies: supposing a uall: [x:A]. B[x] equal: t ∈ T
Lemmas :  es-causle_antisymmetry es-causle_weakening_locl es-le_wf es-E_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[e,e':E].    (e  =  e')  supposing  (e'  \mleq{}loc  e    and  e  \mleq{}loc  e'  )



Date html generated: 2015_07_17-AM-08_38_58
Last ObjectModification: 2015_01_27-PM-02_41_55

Home Index