---

Step * 2 1 1 of Lemma hdf-union-ap

.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. a : A
6. valueall-type(C)
7. valueall-type(B)
8. ↑hdf-halted(X)
9. x : A ─→ (hdataflow(A;C) × bag(C))@i
10. z1 : hdataflow(A;C)@i
11. ¬↑hdf-halted(z1)
12. z2 : bag(C)@i
13. (x a) = <z1, z2> ∈ (hdataflow(A;C) × bag(C))@i
14. ff ∈ 𝔹
15. a1 : A@i
16. v1 : hdataflow(A;C)@i
17. v2 : bag(C)@i
18. z1(a1) = <v1, v2> ∈ (hdataflow(A;C) × bag(C))@i
19. v : bag(B + C)@i
20. bag-map(λx.(inr x );v2) = v ∈ bag(B + C)@i
⊢ mk-hdf(XY,a.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>;XY.let X,Y = XY 
                                          in hdf-halted(X) ∧b hdf-halted(Y);<hdf-halt(), v1>) ∈ hdataflow(A;B + C)
BY
{ (InstLemma `hdf-union_wf` [⌈A⌉;⌈B⌉;⌈C⌉]⋅ THENA Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. a : A
6. valueall-type(C)
7. valueall-type(B)
8. ↑hdf-halted(X)
9. x : A ─→ (hdataflow(A;C) × bag(C))@i
10. z1 : hdataflow(A;C)@i
11. ¬↑hdf-halted(z1)
12. z2 : bag(C)@i
13. (x a) = <z1, z2> ∈ (hdataflow(A;C) × bag(C))@i
14. ff ∈ 𝔹
15. a1 : A@i
16. v1 : hdataflow(A;C)@i
17. v2 : bag(C)@i
18. z1(a1) = <v1, v2> ∈ (hdataflow(A;C) × bag(C))@i
19. v : bag(B + C)@i
20. bag-map(λx.(inr x );v2) = v ∈ bag(B + C)@i
21. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
      (X + Y ∈ hdataflow(A;B + C)) supposing (valueall-type(B) and valueall-type(C))
⊢ mk-hdf(XY,a.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>;XY.let X,Y = XY 
                                          in hdf-halted(X) ∧b hdf-halted(Y);<hdf-halt(), v1>) ∈ hdataflow(A;B + C)

---

Latex:


.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  X  :  hdataflow(A;B)
5.  a  :  A
6.  valueall-type(C)
7.  valueall-type(B)
8.  \muparrow{}hdf-halted(X)
9.  x  :  A  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))@i
10.  z1  :  hdataflow(A;C)@i
11.  \mneg{}\muparrow{}hdf-halted(z1)
12.  z2  :  bag(C)@i
13.  (x  a)  =  <z1,  z2>@i
14.  ff  \mmember{}  \mBbbB{}
15.  a1  :  A@i
16.  v1  :  hdataflow(A;C)@i
17.  v2  :  bag(C)@i
18.  z1(a1)  =  <v1,  v2>@i
19.  v  :  bag(B  +  C)@i
20.  bag-map(\mlambda{}x.(inr  x  );v2)  =  v@i
\mvdash{}  mk-hdf(XY,a.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>XY.let  X,Y  =  XY 
                                                                                    in  hdf-halted(X)  \mwedge{}\msubb{}  hdf-halted(Y);<hdf-halt(),  v1>)  \mmember{}  hdat\000Caflow(A;B  +  C)


By

(InstLemma  `hdf-union\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index