---

Step * of Lemma OARcast_init_odstate_wf

∀[M:ValueAllType]. ∀[orderers:bag(Id)].  (OARcast_init_odstate(M;orderers) ∈ bag(Id) × ((M × ℕ) List))
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[M:ValueAllType].  \mforall{}[orderers:bag(Id)].
    (OARcast\_init\_odstate(M;orderers)  \mmember{}  bag(Id)  \mtimes{}  ((M  \mtimes{}  \mBbbN{})  List))


By

---

Latex:
ProveEmlWfLemma

---

Home Index