---

Step * 1 of Lemma eclass2-program_wf


1. Info : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. X : EClass(B ─→ bag(C))
6. Y : EClass(B)
7. F : Id ─→ hdataflow(Info;B ─→ bag(C))
8. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B ─→ bag(C)))
9. G : Id ─→ hdataflow(Info;B)
10. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(G loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
11. es : EO+(Info)@i'
12. e : E@i
⊢ (X o Y)(e) = (snd((λi.((F i) o (G i))) loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(C)
BY
{ (RepUR ``eclass2 class-ap`` 0
   THEN Fold `class-ap` 0
   THEN (RWO "-5 -3" 0 THEN Auto)
   THEN GenConclAtAddr [3;1;1;2]
   THEN Thin (-1)
   THEN RenameVar `L' (-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 `h' (-1)
         THEN (GenConclAtAddr [3;1;1;1;1]⋅
               THEN Thin (-1)
               THEN RenameVar `g' (-1)
               THEN ThinVars [`X';`Y';`es';`e';`F';`G'])⋅)⋅) }

1
1. Info : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. L : Info List@i
6. x : Info@i
7. h : hdataflow(Info;B)@i
8. g : hdataflow(Info;B ─→ bag(C))@i
⊢ ∪f∈snd(g*(L)(x)).∪b∈snd(h*(L)(x)).f b = (snd(g o h*(L)(x))) ∈ bag(C)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  C  :  Type
4.  valueall-type(C)
5.  X  :  EClass(B  {}\mrightarrow{}  bag(C))
6.  Y  :  EClass(B)
7.  F  :  Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  bag(C))
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(F  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
9.  G  :  Id  {}\mrightarrow{}  hdataflow(Info;B)
10.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (Y(e)  =  (snd(G  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
11.  es  :  EO+(Info)@i'
12.  e  :  E@i
\mvdash{}  (X  o  Y)(e)  =  (snd((\mlambda{}i.((F  i)  o  (G  i)))  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e))))


By

---

Latex:
(RepUR  ``eclass2  class-ap``  0
  THEN  Fold  `class-ap`  0
  THEN  (RWO  "-5  -3"  0  THEN  Auto)
  THEN  GenConclAtAddr  [3;1;1;2]
  THEN  Thin  (-1)
  THEN  RenameVar  `L'  (-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  `h'  (-1)
              THEN  (GenConclAtAddr  [3;1;1;1;1]\mcdot{}
                          THEN  Thin  (-1)
                          THEN  RenameVar  `g'  (-1)
                          THEN  ThinVars  [`X';`Y';`es';`e';`F';`G'])\mcdot{})\mcdot{})

---

Home Index