---

Step * 1 of Lemma hdf-union-ap


1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. a : A
7. valueall-type(C)
8. valueall-type(B)
9. ↑hdf-halted(X)
10. ↑hdf-halted(Y)
⊢ <hdf-halt(), {}> = <hdf-halt(), {}> ∈ (hdataflow(A;B + C) × bag(B + C))
BY
{ Auto }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  X  :  hdataflow(A;B)
5.  Y  :  hdataflow(A;C)
6.  a  :  A
7.  valueall-type(C)
8.  valueall-type(B)
9.  \muparrow{}hdf-halted(X)
10.  \muparrow{}hdf-halted(Y)
\mvdash{}  <hdf-halt(),  \{\}>  =  <hdf-halt(),  \{\}>


By

Auto

---

Home Index