---

{ [es:EO]. [p:E  (E + Top)].
    [a,b,c:E].
      (same-thread(es;p;a;c)) supposing 
         (same-thread(es;p;b;c) and 
         same-thread(es;p;a;b)) 
    supposing 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,  es-E_wf,  causal-predecessor_wf,  top_wf,  event_ordering_wf

---

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


Date html generated: 2011_08_16-AM-11_16_58
Last ObjectModification: 2011_06_20-AM-00_22_39

Home Index