---

Step * 2 of Lemma hdf-union-ap


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. z2 : bag(C)@i
12. (x a) = <z1, z2> ∈ (hdataflow(A;C) × bag(C))@i
⊢ let s1,b = let out ←─ bag-map(λx.(inr x );z2)
             in <<hdf-halt(), z1>, 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
     >
= <if hdf-halted(z1)
   then hdf-halt()
   else hdf-run(λa1.let s1,b = let Y',ys = z1(a1) 
                               in let out ←─ bag-map(λx.(inr x );ys)
                                  in <<hdf-halt(), 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
                       >)
   fi 
  , bag-map(λx.(inr x );z2)
  >
∈ (hdataflow(A;B + C) × bag(B + C))
BY
{ ((CallByValueReduceOn ⌈bag-map(λx.(inr x );z2)⌉ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN EqCD
   THEN Auto
   THEN RW (AddrC [2] RecUnfoldTopAbC) 0
   THEN Reduce 0
   THEN Fold `member` 0
   THEN 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
⊢ let s1,b = let Y',ys = z1(a1) 
             in let out ←─ bag-map(λx.(inr x );ys)
                in <<hdf-halt(), 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)

---

Latex:



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.  z2  :  bag(C)@i
12.  (x  a)  =  <z1,  z2>@i
\mvdash{}  let  s1,b  =  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inr  x  );z2)
                          in  <<hdf-halt(),  z1>,  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
          >
=  <if  hdf-halted(z1)
      then  hdf-halt()
      else  hdf-run(\mlambda{}a1.let  s1,b  =  let  Y',ys  =  z1(a1) 
                                                              in  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inr  x  );ys)
                                                                    in  <<hdf-halt(),  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
                                              >)
      fi 
    ,  bag-map(\mlambda{}x.(inr  x  );z2)
    >


By

((CallByValueReduceOn  \mkleeneopen{}bag-map(\mlambda{}x.(inr  x  );z2)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto
  THEN  RW  (AddrC  [2]  RecUnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  Fold  `member`  0
  THEN  Auto)

---

Home Index