Step
*
of Lemma
es-class-causal-rel_wf
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[R:E(X) ─→ A ─→ B ─→ ℙ].
  (e∈X(x) 
⇐c
⇒ Y(y) such that
    R[e;x;y] ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[R:E(X)  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    (e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  Y(y)  such  that
        R[e;x;y]  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index