---

Step * of Lemma hdf-halt_wf

∀[A,B:Type].  (hdf-halt() ∈ hdataflow(A;B))
BY
{ (ProveWfLemma
   THEN (InstLemma `hdataflow-ext` [⌈A⌉;⌈B⌉]⋅ THENA Auto)
   THEN SubsumeC ⌈A ─→ (hdataflow(A;B) × bag(B))?⌉⋅
   THEN Auto) }

---

Latex:


\mforall{}[A,B:Type].    (hdf-halt()  \mmember{}  hdataflow(A;B))


By

(ProveWfLemma
  THEN  (InstLemma  `hdataflow-ext`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))?\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index