---

Step * of Lemma eclass1-program-wf-hdf

∀[Info,B,C:Type].
  ∀[f:Id ⟶ B ⟶ C]. ∀[pr:Id ⟶ hdataflow(Info;B)].  (eclass1-program(f;pr) ∈ Id ⟶ hdataflow(Info;C)) 
  supposing valueall-type(C)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].
    \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (eclass1-program(f;pr)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;C)) 
    supposing  valueall-type(C)


By

---

Latex:
ProveWfLemma

---

Home Index