---

Step * of Lemma oar-consistency_wf

∀[Info:Type]
  ∀es:EO+(Info). ∀M:Type. ∀correct:Id ⟶ ℙ. ∀OARDeliver:EClass(Id × ℕ × M).
    (oar-consistency(es;M;correct;OARDeliver) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}M:Type.  \mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}OARDeliver:EClass(Id  \mtimes{}  \mBbbN{}  \mtimes{}  M).
        (oar-consistency(es;M;correct;OARDeliver)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index