---

Step * of Lemma parallel-class-program_wf

∀[Info,B:Type].
  ∀[X,Y:EClass(B)]. ∀[Xpr:LocalClass(X)]. ∀[Ypr:LocalClass(Y)].  (Xpr || Ypr ∈ LocalClass(X || Y)) 
  supposing valueall-type(B)
BY
{ (Auto
   THEN D (-2)
   THEN D (-1)
   THEN RepUR ``parallel-class-program`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Reduce 0
   THEN RepUR ``parallel-class eclass-compose2 class-ap`` 0
   THEN Fold `class-ap` 0
   THEN (RWO "-5" 0 THENA Auto)
   THEN (RWO "-3" 0 THENA Auto)
   THEN GenConclAtAddr [3;1;1;2]
   THEN Thin (-1)
   THEN GenConclAtAddr [3;1;2]
   THEN Thin (-1)
   THEN RenameVar `x' (-1)
   THEN GenConclAtAddr [3;1;1;1;2]⋅
   THEN Thin (-1)
   THEN RenameVar `ypr' (-1)
   THEN GenConclAtAddr [3;1;1;1;1]⋅
   THEN Thin (-1)
   THEN RenameVar `xpr' (-1)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (HDataflowHD (-1) THENA Auto)
   THEN (HDataflowHD (-2) THENA Auto)
   THEN RepUR ``hdf-parallel`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN RepUR ``hdf-halted hdf-ap hdf-halt hdf-run`` 0
   THEN Auto
   THEN Try ((Fold `hdf-halt` 0 THEN (RWW "iterate-hdf-halt" 0⋅ THENA Auto) THEN RepUR ``hdf-halt`` 0 THEN Auto))
   THEN Try (Folds ``hdf-ap hdf-halted`` 0)) }

1
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. x : Info@i
13. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
14. x2 : Info ─→ (hdataflow(Info;B) × bag(B))@i
⊢ ((snd((x1 x))) + (snd((x2 x))))
= (snd(let s1,b = let X',xs = x1 x 
                  in let Y',ys = x2 x 
                     in let out ←─ xs + 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 ←─ xs + ys
                                in <<X', Y'>, out>;XY.let X,Y = XY 
                                                   in hdf-halted(X) ∧b hdf-halted(Y);s1)
          , b
          >))
∈ bag(B)

2
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. x : Info@i
13. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
14. y : Unit@i
⊢ ((snd((x1 x))) + {})
= (snd(let s1,b = let X',xs = x1 x 
                  in let out ←─ 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 ←─ xs + ys
                                in <<X', Y'>, out>;XY.let X,Y = XY 
                                                   in hdf-halted(X) ∧b hdf-halted(Y);s1)
          , b
          >))
∈ bag(B)

3
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. x : Info@i
13. y : Unit@i
14. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
⊢ (snd((x1 x)))
= (snd(let s1,b = let Y',ys = x1 x 
                  in let out ←─ ys
                     in <<inr ⋅ , 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 ←─ xs + ys
                                in <<X', Y'>, out>;XY.let X,Y = XY 
                                                   in hdf-halted(X) ∧b hdf-halted(Y);s1)
          , b
          >))
∈ bag(B)

4
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. u : Info@i
13. v : Info List@i
14. ∀x:Info. ∀ypr,xpr:hdataflow(Info;B).
      (((snd(xpr*(v)(x))) + (snd(ypr*(v)(x)))) = (snd(xpr || ypr*(v)(x))) ∈ bag(B))@i
15. x : Info@i
16. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
17. x2 : Info ─→ (hdataflow(Info;B) × bag(B))@i
⊢ ((snd(fst((x1 u))*(v)(x))) + (snd(fst((x2 u))*(v)(x))))
= (snd(fst(let s1,b = let X',xs = x1 u 
                      in let Y',ys = x2 u 
                         in let out ←─ xs + 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 ←─ xs + ys
                                    in <<X', Y'>, out>;XY.let X,Y = XY 
                                                       in hdf-halted(X) ∧b hdf-halted(Y);s1)
              , b
              >)*(v)(x)))
∈ bag(B)

5
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. u : Info@i
13. v : Info List@i
14. ∀x:Info. ∀ypr,xpr:hdataflow(Info;B).
      (((snd(xpr*(v)(x))) + (snd(ypr*(v)(x)))) = (snd(xpr || ypr*(v)(x))) ∈ bag(B))@i
15. x : Info@i
16. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
17. y : Unit@i
⊢ ((snd(fst((x1 u))*(v)(x))) + {})
= (snd(fst(let s1,b = let X',xs = x1 u 
                      in let out ←─ 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 ←─ xs + ys
                                    in <<X', Y'>, out>;XY.let X,Y = XY 
                                                       in hdf-halted(X) ∧b hdf-halted(Y);s1)
              , b
              >)*(v)(x)))
∈ bag(B)

6
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B)
5. Y : EClass(B)
6. Xpr : Id ─→ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(Xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. Ypr : Id ─→ hdataflow(Info;B)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(Ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
10. es : EO+(Info)@i'
11. e : E@i
12. u : Info@i
13. v : Info List@i
14. ∀x:Info. ∀ypr,xpr:hdataflow(Info;B).
      (((snd(xpr*(v)(x))) + (snd(ypr*(v)(x)))) = (snd(xpr || ypr*(v)(x))) ∈ bag(B))@i
15. x : Info@i
16. y : Unit@i
17. x1 : Info ─→ (hdataflow(Info;B) × bag(B))@i
⊢ (snd(fst((x1 u))*(v)(x)))
= (snd(fst(let s1,b = let Y',ys = x1 u 
                      in let out ←─ ys
                         in <<inr ⋅ , 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 ←─ xs + ys
                                    in <<X', Y'>, out>;XY.let X,Y = XY 
                                                       in hdf-halted(X) ∧b hdf-halted(Y);s1)
              , b
              >)*(v)(x)))
∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[X,Y:EClass(B)].  \mforall{}[Xpr:LocalClass(X)].  \mforall{}[Ypr:LocalClass(Y)].    (Xpr  ||  Ypr  \mmember{}  LocalClass(X  ||  Y)) 
    supposing  valueall-type(B)


By

---

Latex:
(Auto
  THEN  D  (-2)
  THEN  D  (-1)
  THEN  RepUR  ``parallel-class-program``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Reduce  0
  THEN  RepUR  ``parallel-class  eclass-compose2  class-ap``  0
  THEN  Fold  `class-ap`  0
  THEN  (RWO  "-5"  0  THENA  Auto)
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  GenConclAtAddr  [3;1;1;2]
  THEN  Thin  (-1)
  THEN  GenConclAtAddr  [3;1;2]
  THEN  Thin  (-1)
  THEN  RenameVar  `x'  (-1)
  THEN  GenConclAtAddr  [3;1;1;1;2]\mcdot{}
  THEN  Thin  (-1)
  THEN  RenameVar  `ypr'  (-1)
  THEN  GenConclAtAddr  [3;1;1;1;1]\mcdot{}
  THEN  Thin  (-1)
  THEN  RenameVar  `xpr'  (-1)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (HDataflowHD  (-1)  THENA  Auto)
  THEN  (HDataflowHD  (-2)  THENA  Auto)
  THEN  RepUR  ``hdf-parallel``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  RepUR  ``hdf-halted  hdf-ap  hdf-halt  hdf-run``  0
  THEN  Auto
  THEN  Try  ((Fold  `hdf-halt`  0
                        THEN  (RWW  "iterate-hdf-halt"  0\mcdot{}  THENA  Auto)
                        THEN  RepUR  ``hdf-halt``  0
                        THEN  Auto))
  THEN  Try  (Folds  ``hdf-ap  hdf-halted``  0))

---

Home Index