### Nuprl Lemma : thread-ordered

`∀es:EO. ∀p:E ─→ (E + Top).`
`  ((causal-predecessor(es;p) ∧ p-inject(E;E;p))`
`  `` (∀e,e':E.  ((e < e') ∨ (e = e' ∈ E)) ∨ (e' < e) supposing same-thread(es;p;e;e')))`

Proof

Definitions occuring in Statement :  same-thread: `same-thread(es;p;e;e')` causal-predecessor: `causal-predecessor(es;p)` es-causl: `(e < e')` es-E: `E` event_ordering: `EO` uimplies: `b supposing a` top: `Top` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` function: `x:A ─→ B[x]` union: `left + right` equal: `s = t ∈ T` p-inject: `p-inject(A;B;f)`
Lemmas :  same-thread_wf es-E_wf causal-predecessor_wf p-inject_wf top_wf event_ordering_wf thread-p-ordered equal_wf es-causl_wf or_wf es-causl_weakening_p-locl
\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).
((causal-predecessor(es;p)  \mwedge{}  p-inject(E;E;p))
{}\mRightarrow{}  (\mforall{}e,e':E.    ((e  <  e')  \mvee{}  (e  =  e'))  \mvee{}  (e'  <  e)  supposing  same-thread(es;p;e;e')))

Date html generated: 2015_07_17-AM-09_09_13
Last ObjectModification: 2015_01_27-PM-00_45_42

Home Index