---

Step * of Lemma same-thread_inversion

∀[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))
BY
{ (Auto THEN (FLemma `causal-pred-wellfounded` [5]) THEN Auto THEN ParallelOp -2) }

---

Latex:


\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))


By

(Auto  THEN  (FLemma  `causal-pred-wellfounded`  [5])  THEN  Auto  THEN  ParallelOp  -2)

---

Home Index