---

Step * 1 1 of Lemma hdf-union-eq-disju


1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. valueall-type(B)
6. X : hdataflow(A;B)@i
7. Y : hdataflow(A;C)@i
⊢ hdf-halted(X + Y) = hdf-halted((λx.(inl x)) o X || (λx.(inr x )) o Y)
BY
{ (RepUR ``hdf-union hdf-parallel hdf-compose1`` 0 THEN RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Repeat (AutoSplit)) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  valueall-type(C)
5.  valueall-type(B)
6.  X  :  hdataflow(A;B)@i
7.  Y  :  hdataflow(A;C)@i
\mvdash{}  hdf-halted(X  +  Y)  =  hdf-halted((\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y)


By

(RepUR  ``hdf-union  hdf-parallel  hdf-compose1``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit))

---

Home Index