---

Step * of Lemma hdf-running_wf

∀[A,B:Type]. ∀[P:hdataflow(A;B)].  (hdf-running(P) ∈ 𝔹)
BY
{ (ProveWfLemma
   THEN GenConcl ⌈P = Q ∈ (A ─→ (hdataflow(A;B) × bag(B))?)⌉⋅
   THEN Auto
   THEN (InstLemma `hdataflow-ext` [⌈A⌉;⌈B⌉]⋅ THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:


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


By

(ProveWfLemma
  THEN  GenConcl  \mkleeneopen{}P  =  Q\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `hdataflow-ext`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index