---

Step * 2 1 1 of Lemma hdf-until-halt-right


1. A : Type
2. B : Type
3. X : hdataflow(A;B)@i
4. a : A@i
5. ↑hdf-halted(X)
⊢ {} = hdf-out(X;a) ∈ bag(B)
BY
{ ((FLemma `hdf-halted-is-inr` [-1] THENA Auto)
   THEN Fold `hdf-halt` (-1)
   THEN HypSubst (-1) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  X  :  hdataflow(A;B)@i
4.  a  :  A@i
5.  \muparrow{}hdf-halted(X)
\mvdash{}  \{\}  =  hdf-out(X;a)


By

((FLemma  `hdf-halted-is-inr`  [-1]  THENA  Auto)
  THEN  Fold  `hdf-halt`  (-1)
  THEN  HypSubst  (-1)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index