---

Step * of Lemma hdf-until-halt-right

∀[A,B:Type]. ∀[X:hdataflow(A;B)].  (hdf-until(X;hdf-halt()) = X ∈ hdataflow(A;B))
BY
{ (Auto THEN RWO "hdataflow-equal" 0 THEN Auto THEN Try ((Using [`C',⌈Top⌉] (BLemma `hdf-until_wf`)⋅ THEN Auto))) }

1
1. A : Type
2. B : Type
3. X : hdataflow(A;B)
4. inputs : A List
⊢ hdf-halted(hdf-until(X;hdf-halt())*(inputs)) = hdf-halted(X*(inputs))

2
1. A : Type
2. B : Type
3. X : hdataflow(A;B)
4. inputs : A List
5. hdf-halted(hdf-until(X;hdf-halt())*(inputs)) = hdf-halted(X*(inputs))
6. a : A
⊢ hdf-out(hdf-until(X;hdf-halt())*(inputs);a) = hdf-out(X*(inputs);a) ∈ bag(B)

---

Latex:


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


By

(Auto
  THEN  RWO  "hdataflow-equal"  0
  THEN  Auto
  THEN  Try  ((Using  [`C',\mkleeneopen{}Top\mkleeneclose{}]  (BLemma  `hdf-until\_wf`)\mcdot{}  THEN  Auto)))

---

Home Index