---

{ [es:EO]. [p:E  (E + Top)]. [e,e':E].
    (same-thread(es;p;e';e)) supposing 
       (same-thread(es;p;e;e') and 
       causal-predecessor(es;p)) }

{ Proof }

---

Definitions occuring in Statement :  same-thread: same-thread(es;p;e;e'),  causal-predecessor: causal-predecessor(es;p),  es-E: E,  event_ordering: EO,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  function: x:A  B[x],  union: left + right
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  same-thread: same-thread(es;p;e;e'),  member: t  T,  all: x:A. B[x],  implies: P  Q,  prop:
Lemmas :  causal-pred-wellfounded,  same-thread_wf,  causal-predecessor_wf,  es-E_wf,  top_wf,  event_ordering_wf

---

\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].  \mforall{}[e,e':E].
    (same-thread(es;p;e';e))  supposing  (same-thread(es;p;e;e')  and  causal-predecessor(es;p))


Date html generated: 2011_08_16-AM-11_16_53
Last ObjectModification: 2011_06_20-AM-00_22_33

Home Index