---

Step * 1 of Lemma same-thread-do-apply


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
BY
{ (((GenConclAtAddr [2]) THENA Auto) THEN (RecUnfold `final-iterate` (-1)) THEN (SplitOnHypITE (-1)) THEN Auto) }

---

Latex:



1.  es  :  EO
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)
3.  causal-predecessor(es;p)
4.  e  :  E
5.  \muparrow{}can-apply(p;e)
6.  SWellFounded(p-graph(E;p)  y  x)
\mvdash{}  final-iterate(p;e)  =  final-iterate(p;do-apply(p;e))


By

(((GenConclAtAddr  [2])  THENA  Auto)
  THEN  (RecUnfold  `final-iterate`  (-1))
  THEN  (SplitOnHypITE  (-1))
  THEN  Auto)

---

Home Index