---

Step * of Lemma parallel-class-program-wf-hdf

∀[A,B:Type].  ∀[Xpr,Ypr:Id ─→ hdataflow(A;B)].  (Xpr || Ypr ∈ Id ─→ hdataflow(A;B)) supposing valueall-type(B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[Xpr,Ypr:Id  {}\mrightarrow{}  hdataflow(A;B)].    (Xpr  ||  Ypr  \mmember{}  Id  {}\mrightarrow{}  hdataflow(A;B))  supposing  valueall-type(B)


By

---

Latex:
ProveWfLemma

---

Home Index