---

Step * of Lemma state-class1-program-wf-hdf

∀[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[pr:Id ─→ hdataflow(Info;A)].
  (state-class1-program(init;f;pr) ∈ Id ─→ hdataflow(Info;B)) supposing (valueall-type(B) and (↓B))
BY
{ (ProveWfLemma
   THEN BLemma `loop-class-state-program-wf-hdf`
   THEN Auto
   THEN BLemma `eclass1-program-wf-hdf`
   THEN Auto
   THEN ProveEmlSquash) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;A)].
    (state-class1-program(init;f;pr)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B))  supposing  (valueall-type(B)  and  (\mdownarrow{}B))


By

---

Latex:
(ProveWfLemma
  THEN  BLemma  `loop-class-state-program-wf-hdf`
  THEN  Auto
  THEN  BLemma  `eclass1-program-wf-hdf`
  THEN  Auto
  THEN  ProveEmlSquash)

---

Home Index