---

Step * 1 of Lemma hdf-union_wf

.....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)
BY
{ (D -2 THEN Reduce 0) }

1
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
⊢ let X',xs = X1(a) 
  in let Y',ys = X2(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:


.....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)  \mtimes{}  hdataflow(A;C)@i
9.  a  :  A@i
\mvdash{}  let  X,Y  =  XY 
    in  let  X',xs  =  X(a) 
          in  let  Y',ys  =  Y(a) 
                in  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inl  x);xs)  +  bag-map(\mlambda{}x.(inr  x  );ys)
                      in  <<X',  Y'>,  out>  \mmember{}  hdataflow(A;B)  \mtimes{}  hdataflow(A;C)  \mtimes{}  bag(B  +  C)


By

(D  -2  THEN  Reduce  0)

---

Home Index