---

Step * of Lemma hdf-union-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
  (X + Y(a)
     = <fst(X(a)) + fst(Y(a)), bag-map(λx.(inl x);snd(X(a))) + bag-map(λx.(inr x );snd(Y(a)))>
     ∈ (hdataflow(A;B + C) × bag(B + C))) supposing 
     (valueall-type(B) and 
     valueall-type(C))
BY
{ (Auto
   THEN RepUR ``hdf-union hdf-ap`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Fold `hdf-ap` 0
   THEN ((BoolCase ⌈hdf-halted(X)⌉⋅ THENA Auto)
         THENL [((Subst' X ~ hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt`  THEN Auto)) THEN Reduce 0)
               ; HDataflowHDVar' `X']
   )
   THEN ((BoolCase ⌈hdf-halted(Y)⌉⋅ THENA Auto)
         THENL [((Subst' Y ~ hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt`  THEN Auto)) THEN Reduce 0)
               ; HDataflowHDVar' `Y']
   )) }

1
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. a : A
7. valueall-type(C)
8. valueall-type(B)
9. ↑hdf-halted(X)
10. ↑hdf-halted(Y)
⊢ <hdf-halt(), {}> = <hdf-halt(), {}> ∈ (hdataflow(A;B + C) × bag(B + C))

2
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))

3
1. A : Type
2. B : Type
3. C : Type
4. Y : hdataflow(A;C)
5. a : A
6. valueall-type(C)
7. valueall-type(B)
8. x : A ─→ (hdataflow(A;B) × bag(B))@i
9. z1 : hdataflow(A;B)@i
10. z2 : bag(B)@i
11. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
12. ↑hdf-halted(Y)
⊢ let s1,b = let out ←─ bag-map(λx.(inl x);z2) + {}
             in <<z1, inr ⋅ >, 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) ∧b tt
   then hdf-halt()
   else hdf-run(λa1.let s1,b = let X',xs = z1(a1) 
                               in let out ←─ bag-map(λx.(inl x);xs) + {}
                                  in <<X', inr ⋅ >, 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.(inl x);z2) + {}
  >
∈ (hdataflow(A;B + C) × bag(B + C))

4
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. z4 : bag(C)@i
14. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
⊢ let s1,b = let out ←─ bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)
             in <<z1, z3>, 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) ∧b hdf-halted(z3)
   then hdf-halt()
   else hdf-run(λa1.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
                       >)
   fi 
  , bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)
  >
∈ (hdataflow(A;B + C) × bag(B + C))

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].  \mforall{}[a:A].
    (X  +  Y(a)
          =  <fst(X(a))  +  fst(Y(a))
              ,  bag-map(\mlambda{}x.(inl  x);snd(X(a)))  +  bag-map(\mlambda{}x.(inr  x  );snd(Y(a)))
              >)  supposing 
          (valueall-type(B)  and 
          valueall-type(C))


By

(Auto
  THEN  RepUR  ``hdf-union  hdf-ap``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Fold  `hdf-ap`  0
  THEN  ((BoolCase  \mkleeneopen{}hdf-halted(X)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((Subst'  X  \msim{}  hdf-halt()  0  THENA  (BLemma  `hdf-halted-is-halt`    THEN  Auto))
                              THEN  Reduce  0
                              )
                          ;  HDataflowHDVar'  `X']
  )
  THEN  ((BoolCase  \mkleeneopen{}hdf-halted(Y)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((Subst'  Y  \msim{}  hdf-halt()  0  THENA  (BLemma  `hdf-halted-is-halt`    THEN  Auto))
                              THEN  Reduce  0
                              )
                          ;  HDataflowHDVar'  `Y']
  ))

---

Home Index