---

Step * of Lemma eclass2-program-wf-hdf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index