---

Step * 1 of Lemma same-thread_transitivity


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
BY
{ (Unfold `same-thread` -3 THEN Auto)⋅ }

---

Latex:



1.  es  :  EO
2.  p  :  E  {}\mrightarrow{}  (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)
9.  SWellFounded(p-graph(E;p)  y  x)
\mvdash{}  final-iterate(p;a)  =  final-iterate(p;c)


By

(Unfold  `same-thread`  -3  THEN  Auto)\mcdot{}

---

Home Index