---

Step * of Lemma same-thread_transitivity

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

1
1. es : EO
2. p : E ─→ (E + Top)
3. causal-predecessor(es;p)
4. a : E
5. b : E
6. c : E
7. same-thread(es;p;a;b)
8. final-iterate(p;b) = final-iterate(p;c) ∈ E
9. SWellFounded(p-graph(E;p) y x)
⊢ final-iterate(p;a) = final-iterate(p;c) ∈ E

---

Latex:


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


By

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

---

Home Index