---

Step * of Lemma msgs-interface-with-omissions-sub_wf

∀[f:Name ─→ Type]
  ∀X:EClass(Interface). ∀failures:ℤ. ∀ids:bag(Id).  (msgs-interface-with-omissions-sub{i:l}(X;failures;ids;f) ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type]
    \mforall{}X:EClass(Interface).  \mforall{}failures:\mBbbZ{}.  \mforall{}ids:bag(Id).
        (msgs-interface-with-omissions-sub\{i:l\}(X;failures;ids;f)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index