---

Step * of Lemma es-class-mcast-fail_wf

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:Id List]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[R:E(X) ─→ A ─→ B ─→ ℙ]. ∀[l:Id List].
  (∀e,x,y. e∈X(x) mcast to each of l a
                         Y(y) such that
                         R[e;x;y]
                        unless loc(e) ∈ f ∈ ℙ)
BY
{ ProveWfLemma⋅ }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Id  List].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[R:E(X)
                                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                                          {}\mrightarrow{}  B
                                                                                                                                                                          {}\mrightarrow{}  \mBbbP{}].
\mforall{}[l:Id  List].
    (\mforall{}e,x,y.  e\mmember{}X(x)  mcast  to  each  of  l  a
                                                  Y(y)  such  that
                                                  R[e;x;y]
                                                unless  loc(e)  \mmember{}  f  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma\mcdot{}

---

Home Index