---

Step * of Lemma loop-class-state-program-wf-hdf

∀[Info,B:Type].
  ∀[init:Id ⟶ bag(B)]. ∀[pr:Id ⟶ hdataflow(Info;B ⟶ B)].
    (loop-class-state-program(pr;init) ∈ Id ⟶ hdataflow(Info;B)) 
  supposing valueall-type(B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  B)].
        (loop-class-state-program(pr;init)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B)) 
    supposing  valueall-type(B)


By

---

Latex:
ProveWfLemma

---

Home Index