---

Step * of Lemma hdf-rec-bind_wf

∀[A,B,C:Type]. ∀[X:C ─→ hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;C)].
  (hdf-rec-bind(X;Y) ∈ C ─→ hdataflow(A;B)) supposing (valueall-type(B) and valueall-type(C))
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:C  {}\mrightarrow{}  hdataflow(A;B)].  \mforall{}[Y:C  {}\mrightarrow{}  hdataflow(A;C)].
    (hdf-rec-bind(X;Y)  \mmember{}  C  {}\mrightarrow{}  hdataflow(A;B))  supposing  (valueall-type(B)  and  valueall-type(C))


By

ProveWfLemma

---

Home Index