### Nuprl Lemma : es-locless-property

`∀es:EO. ∀x,y:es-base-E(es).`
`  ((loc(x) = loc(y) ∈ Id)`
`  `` (((x < y) `⇐⇒` ↑es-locless(es;x;y))`
`     ∧ ((¬↑es-locless(es;x;y)) `` (¬↑es-locless(es;y;x)) `` (x = y ∈ es-base-E(es)))))`

Proof

Definitions occuring in Statement :  es-locless: `es-locless(es;e1;e2)` es-causl: `(e < e')` es-loc: `loc(e)` es-base-E: `es-base-E(es)` event_ordering: `EO` Id: `Id` assert: `↑b` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` equal: `s = t ∈ T`
Lemmas :  event_ordering_properties es-loc-wf-base es-locless-wf-base es-causl-wf-base not_wf assert_wf equal_wf Id_wf es-base-E_wf event_ordering_wf
\mforall{}es:EO.  \mforall{}x,y:es-base-E(es).
((loc(x)  =  loc(y))
{}\mRightarrow{}  (((x  <  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(es;x;y))
\mwedge{}  ((\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y))))

Date html generated: 2015_07_17-AM-08_34_25
Last ObjectModification: 2015_01_27-PM-02_59_08

Home Index