---

Step * of Lemma hdf-run_wf

∀[A,B:Type]. ∀[P:A ─→ (hdataflow(A;B) × bag(B))].  (hdf-run(P) ∈ 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].  \mforall{}[P:A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))].    (hdf-run(P)  \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