---

Step * of Lemma hdf-union_wf

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
  (X + Y ∈ hdataflow(A;B + C)) supposing (valueall-type(B) and valueall-type(C))
BY
{ (Intros THEN Unhide⋅ THEN Unfold `hdf-union` 0 THEN MemCD THEN Try (QuickAuto)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. valueall-type(C)
7. valueall-type(B)
8. XY : hdataflow(A;B) × hdataflow(A;C)@i
9. a : A@i
⊢ let X,Y = XY 
  in let X',xs = X(a) 
     in let Y',ys = Y(a) 
        in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
           in <<X', Y'>, out> ∈ hdataflow(A;B) × hdataflow(A;C) × bag(B + C)

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].
    (X  +  Y  \mmember{}  hdataflow(A;B  +  C))  supposing  (valueall-type(B)  and  valueall-type(C))


By

(Intros  THEN  Unhide\mcdot{}  THEN  Unfold  `hdf-union`  0  THEN  MemCD  THEN  Try  (QuickAuto))

---

Home Index