Nuprl Lemma : es-causl-total

es:EO. ∀e,e':E.  (e e' ∈ E) ∨ (e < e') ∨ (e' < e) supposing loc(e) loc(e') ∈ Id


Proof




Definitions occuring in Statement :  es-causl: (e < e') es-loc: loc(e) es-E: E event_ordering: EO Id: Id uimplies: supposing a all: x:A. B[x] or: P ∨ Q equal: t ∈ T
Lemmas :  assert_wf es-dom_wf
\mforall{}es:EO.  \mforall{}e,e':E.    (e  =  e')  \mvee{}  (e  <  e')  \mvee{}  (e'  <  e)  supposing  loc(e)  =  loc(e')



Date html generated: 2015_07_17-AM-08_34_40
Last ObjectModification: 2015_01_27-PM-02_59_04

Home Index