---

Step * 1 of Lemma same-thread_wf


1. es : EO
2. p : E ─→ (E + Top)
3. causal-predecessor(es;p)
4. e : E
5. e' : E
⊢ same-thread(es;p;e;e') ∈ ℙ
BY
{ ((FLemma `causal-pred-wellfounded` [-3]) THENA Auto) }

1
1. es : EO
2. p : E ─→ (E + Top)
3. causal-predecessor(es;p)
4. e : E
5. e' : E
6. SWellFounded(p-graph(E;p) y x)
⊢ same-thread(es;p;e;e') ∈ ℙ

---

Latex:



1.  es  :  EO
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)
3.  causal-predecessor(es;p)
4.  e  :  E
5.  e'  :  E
\mvdash{}  same-thread(es;p;e;e')  \mmember{}  \mBbbP{}


By

((FLemma  `causal-pred-wellfounded`  [-3])  THENA  Auto)

---

Home Index