---

Step * 2 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
8. a : A@i
⊢ hdf-out(X + Y;a) = hdf-out((λx.(inl x)) o X || (λx.(inr x )) o Y;a) ∈ bag(B + C)
BY
{ (RepUR ``hdf-union hdf-parallel hdf-compose1`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN (RWO "hdf-out-run" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN HDataflowHDAll
   THEN (With ⌈bag(B + C)⌉ (CallByValueReduceAtAddr [2;1;1] 0)⋅ THENA Auto)
   THEN Reduce 0⋅
   THEN Repeat (((CallByValueReduceAtAddr [3;1;1;1;1] 0 THENA Complete (Auto)) THEN Reduce 0))
   THEN (With ⌈bag(B + C)⌉ (CallByValueReduceAtAddr [3;1;1] 0)⋅ THENA Complete (Auto))
   THEN Reduce 0
   THEN Auto) }

---

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
8.  a  :  A@i
\mvdash{}  hdf-out(X  +  Y;a)  =  hdf-out((\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y;a)


By

(RepUR  ``hdf-union  hdf-parallel  hdf-compose1``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  (RWO  "hdf-out-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  HDataflowHDAll
  THEN  (With  \mkleeneopen{}bag(B  +  C)\mkleeneclose{}  (CallByValueReduceAtAddr  [2;1;1]  0)\mcdot{}  THENA  Auto)
  THEN  Reduce  0\mcdot{}
  THEN  Repeat  (((CallByValueReduceAtAddr  [3;1;1;1;1]  0  THENA  Complete  (Auto))  THEN  Reduce  0))
  THEN  (With  \mkleeneopen{}bag(B  +  C)\mkleeneclose{}  (CallByValueReduceAtAddr  [3;1;1]  0)\mcdot{}  THENA  Complete  (Auto))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index