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
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T es-E: E es-base-E: es-base-E(es) uimplies: supposing a or: P ∨ Q prop: uall: [x:A]. B[x] guard: {T} es-dom: es-dom(es)

Latex:
\mforall{}es:EO.  \mforall{}e,e':E.    (e  =  e')  \mvee{}  (e  <  e')  \mvee{}  (e'  <  e)  supposing  loc(e)  =  loc(e')



Date html generated: 2016_05_16-AM-09_15_13
Last ObjectModification: 2015_12_28-PM-09_57_28

Theory : new!event-ordering


Home Index