Nuprl Lemma : es-locl-total

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


Proof




Definitions occuring in Statement :  es-locl: (e <loc 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 :  pes-axioms equal_wf Id_wf es-loc_wf es-E_wf event_ordering_wf
\mforall{}es:EO.  \mforall{}e,e':E.    (e  <loc  e')  \mvee{}  (e  =  e')  \mvee{}  (e'  <loc  e)  supposing  loc(e)  =  loc(e')



Date html generated: 2015_07_17-AM-08_37_52
Last ObjectModification: 2015_01_27-PM-02_57_09

Home Index