---

Step * of Lemma same-thread_weakening

∀[es:EO]. ∀[p:E ⟶ (E + Top)].
  ∀[e,e':E].  same-thread(es;p;e;e') supposing e = e' ∈ E supposing causal-predecessor(es;p)
BY
{ Auto }

1
1. es : EO
2. p : E ⟶ (E + Top)
3. causal-predecessor(es;p)
4. e : E
5. e' : E
6. e = e' ∈ E
⊢ same-thread(es;p;e;e')

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].
    \mforall{}[e,e':E].    same-thread(es;p;e;e')  supposing  e  =  e'  supposing  causal-predecessor(es;p)


By

---

Latex:
Auto

---

Home Index