---

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

∀[Info,A,B:Type].
  ∀[xpr:Id ⟶ hdataflow(Info;A)]. ∀[ypr:A ⟶ Id ⟶ hdataflow(Info;B)].  (xpr >>= ypr ∈ Id ⟶ hdataflow(Info;B)) 
  supposing valueall-type(B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}[xpr:Id  {}\mrightarrow{}  hdataflow(Info;A)].  \mforall{}[ypr:A  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (xpr  >>=  ypr  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B)) 
    supposing  valueall-type(B)


By

---

Latex:
ProveWfLemma

---

Home Index