---

Step * of Lemma same-thread-do-apply

∀[es:EO]. ∀[p:E ─→ (E + Top)].
  ∀[e:E]. same-thread(es;p;e;do-apply(p;e)) supposing ↑can-apply(p;e) supposing causal-predecessor(es;p)
BY
{ (Auto
   THEN Unfold `same-thread` 0
   THEN (Assert ⌈SWellFounded(p-graph(E;p) y x)⌉⋅ THENL [(BLemma `causal-pred-wellfounded` THEN Auto); Id])) }

1
1. es : EO
2. p : E ─→ (E + Top)
3. causal-predecessor(es;p)
4. e : E
5. ↑can-apply(p;e)
6. SWellFounded(p-graph(E;p) y x)
⊢ final-iterate(p;e) = final-iterate(p;do-apply(p;e)) ∈ E

---

Latex:


\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].
    \mforall{}[e:E].  same-thread(es;p;e;do-apply(p;e))  supposing  \muparrow{}can-apply(p;e) 
    supposing  causal-predecessor(es;p)


By

(Auto
  THEN  Unfold  `same-thread`  0
  THEN  (Assert
              \mkleeneopen{}SWellFounded(p-graph(E;p)  y  x)\mkleeneclose{}\mcdot{}
              THENL  [(BLemma  `causal-pred-wellfounded`  THEN  Auto);  Id]
  ))

---

Home Index