---

Step * 4 1 of Lemma hdf-union-ap


1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A ─→ (hdataflow(A;B) × bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
11. x1 : A ─→ (hdataflow(A;C) × bag(C))@i
12. z3 : hdataflow(A;C)@i
13. ¬((↑hdf-halted(z1)) ∧ (↑hdf-halted(z3)))
14. z4 : bag(C)@i
15. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
16. b : bag(B + C)@i
17. (bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)) = b ∈ bag(B + C)@i
18. ff ∈ 𝔹
19. a1 : A@i
⊢ let s1,b = let X',xs = z1(a1) 
             in let Y',ys = z3(a1) 
                in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
                   in <<X', Y'>, out> 
  in <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);s1)
     , b
     > ∈ hdataflow(A;B + C) × bag(B + C)
BY
{ (RepeatFor 2 ((GenConclAtAddr [2;1;1] THEN D -2 THEN Reduce 0))
   THEN (GenConclAtAddrType ⌈bag(B + C)⌉ [2;1;1]⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌈v⌉ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN MemCD) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A ─→ (hdataflow(A;B) × bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
11. x1 : A ─→ (hdataflow(A;C) × bag(C))@i
12. z3 : hdataflow(A;C)@i
13. ¬((↑hdf-halted(z1)) ∧ (↑hdf-halted(z3)))
14. z4 : bag(C)@i
15. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
16. b : bag(B + C)@i
17. (bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)) = b ∈ bag(B + C)@i
18. ff ∈ 𝔹
19. a1 : A@i
20. v1 : hdataflow(A;B)@i
21. v2 : bag(B)@i
22. z1(a1) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
23. v3 : hdataflow(A;C)@i
24. v4 : bag(C)@i
25. z3(a1) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
26. v : bag(B + C)@i
27. (bag-map(λx.(inl x);v2) + bag-map(λx.(inr x );v4)) = 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);<v1, v3>) ∈ hdataflow(A;B + C)

2
.....subterm..... T:t
2:n
1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A ─→ (hdataflow(A;B) × bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
11. x1 : A ─→ (hdataflow(A;C) × bag(C))@i
12. z3 : hdataflow(A;C)@i
13. ¬((↑hdf-halted(z1)) ∧ (↑hdf-halted(z3)))
14. z4 : bag(C)@i
15. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
16. b : bag(B + C)@i
17. (bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)) = b ∈ bag(B + C)@i
18. ff ∈ 𝔹
19. a1 : A@i
20. v1 : hdataflow(A;B)@i
21. v2 : bag(B)@i
22. z1(a1) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
23. v3 : hdataflow(A;C)@i
24. v4 : bag(C)@i
25. z3(a1) = <v3, v4> ∈ (hdataflow(A;C) × bag(C))@i
26. v : bag(B + C)@i
27. (bag-map(λx.(inl x);v2) + bag-map(λx.(inr x );v4)) = v ∈ bag(B + C)@i
⊢ v ∈ bag(B + C)

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  a  :  A
5.  valueall-type(C)
6.  valueall-type(B)
7.  x  :  A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))@i
8.  z1  :  hdataflow(A;B)@i
9.  z2  :  bag(B)@i
10.  (x  a)  =  <z1,  z2>@i
11.  x1  :  A  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))@i
12.  z3  :  hdataflow(A;C)@i
13.  \mneg{}((\muparrow{}hdf-halted(z1))  \mwedge{}  (\muparrow{}hdf-halted(z3)))
14.  z4  :  bag(C)@i
15.  (x1  a)  =  <z3,  z4>@i
16.  b  :  bag(B  +  C)@i
17.  (bag-map(\mlambda{}x.(inl  x);z2)  +  bag-map(\mlambda{}x.(inr  x  );z4))  =  b@i
18.  ff  \mmember{}  \mBbbB{}
19.  a1  :  A@i
\mvdash{}  let  s1,b  =  let  X',xs  =  z1(a1) 
                          in  let  Y',ys  =  z3(a1) 
                                in  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inl  x);xs)  +  bag-map(\mlambda{}x.(inr  x  );ys)
                                      in  <<X',  Y'>,  out> 
    in  <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);s1)
          ,  b
          >  \mmember{}  hdataflow(A;B  +  C)  \mtimes{}  bag(B  +  C)


By

(RepeatFor  2  ((GenConclAtAddr  [2;1;1]  THEN  D  -2  THEN  Reduce  0))
  THEN  (GenConclAtAddrType  \mkleeneopen{}bag(B  +  C)\mkleeneclose{}  [2;1;1]\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  MemCD)

---

Home Index