---

Step * 1 1 1 of Lemma hdf-union_wf


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. X1 : hdataflow(A;B)@i
9. X2 : hdataflow(A;C)@i
10. a : A@i
11. v1 : hdataflow(A;B)@i
12. v2 : bag(B)@i
13. X1(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
14. v3 : hdataflow(A;C)@i
15. v4 : bag(C)@i
16. X2(a) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
⊢ let out ←─ bag-map(λx.(inl x);v2) + bag-map(λx.(inr x );v4)
  in <<v1, v3>, out> ∈ hdataflow(A;B) × hdataflow(A;C) × bag(B + C)
BY
{ GenConclAtAddrType ⌈bag(B + C)⌉ [2;1]⋅ }

1
.....wf..... 
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. X1 : hdataflow(A;B)@i
9. X2 : hdataflow(A;C)@i
10. a : A@i
11. v1 : hdataflow(A;B)@i
12. v2 : bag(B)@i
13. X1(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
14. v3 : hdataflow(A;C)@i
15. v4 : bag(C)@i
16. X2(a) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
⊢ bag-map(λx.(inl x);v2) + bag-map(λx.(inr x );v4) ∈ bag(B + C)

2
.....wf..... 
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. X1 : hdataflow(A;B)@i
9. X2 : hdataflow(A;C)@i
10. a : A@i
11. v1 : hdataflow(A;B)@i
12. v2 : bag(B)@i
13. X1(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
14. v3 : hdataflow(A;C)@i
15. v4 : bag(C)@i
16. X2(a) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
⊢ bag(B + C) ∈ Type

3
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. X1 : hdataflow(A;B)@i
9. X2 : hdataflow(A;C)@i
10. a : A@i
11. v1 : hdataflow(A;B)@i
12. v2 : bag(B)@i
13. X1(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
14. v3 : hdataflow(A;C)@i
15. v4 : bag(C)@i
16. X2(a) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
17. v : bag(B + C)@i
18. (bag-map(λx.(inl x);v2) + bag-map(λx.(inr x );v4)) = v ∈ bag(B + C)@i
⊢ let out ←─ v
  in <<v1, v3>, out> ∈ hdataflow(A;B) × hdataflow(A;C) × bag(B + C)

---

Latex:



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.  X1  :  hdataflow(A;B)@i
9.  X2  :  hdataflow(A;C)@i
10.  a  :  A@i
11.  v1  :  hdataflow(A;B)@i
12.  v2  :  bag(B)@i
13.  X1(a)  =  <v1,  v2>@i
14.  v3  :  hdataflow(A;C)@i
15.  v4  :  bag(C)@i
16.  X2(a)  =  <v3,  v4>@i
\mvdash{}  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inl  x);v2)  +  bag-map(\mlambda{}x.(inr  x  );v4)
    in  <<v1,  v3>,  out>  \mmember{}  hdataflow(A;B)  \mtimes{}  hdataflow(A;C)  \mtimes{}  bag(B  +  C)


By

GenConclAtAddrType  \mkleeneopen{}bag(B  +  C)\mkleeneclose{}  [2;1]\mcdot{}

---

Home Index