---

Step * of Lemma event_ordering_cumulative

EO ⊆r event_ordering{j:l} supposing Type ⊆r 𝕌{j}
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D (-1) THEN At 𝕌{j} MemTypeCD⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
EO  \msubseteq{}r  event\_ordering\{j:l\}  supposing  Type  \msubseteq{}r  \mBbbU{}\{j\}


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  (-1)  THEN  At  \mBbbU{}\{j\}  MemTypeCD\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index