---

Step * of Lemma es-class-reply-or-fail_wf

∀[Info,A,B:Type]. ∀[loc1:A ─→ Id]. ∀[loc2:B ─→ Id]. ∀[es:EO+(Info)]. ∀[f:Id List]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
∀[R:E(X) ─→ A ─→ B ─→ ℙ].
  (∀e,x,y. e∈X(x) ⇐c⇒ ∃ reply Y(y)@loc1[x] such that
                       R[e;x;y]∧loc2[y]=loc(e)
                      unless loc(e) ∈ f ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[loc1:A  {}\mrightarrow{}  Id].  \mforall{}[loc2:B  {}\mrightarrow{}  Id].  \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{}e,x,y.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  reply  Y(y)@loc1[x]  such  that
                                              R[e;x;y]\mwedge{}loc2[y]=loc(e)
                                            unless  loc(e)  \mmember{}  f  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index