---

Step * 1 of Lemma eclass0-program_wf


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

1
1. Info : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. F : Id ─→ B ─→ bag(C)
6. Xpr : Id ─→ hdataflow(Info;B)
7. es : EO+(Info)@i'
8. e : E@i
9. L : Info List@i
10. x : Info@i
11. h : hdataflow(Info;B)@i
⊢ ∪x∈snd(h*(L)(x)).F loc(e) x = (snd(hdf-compose0(F loc(e);h)*(L)(x))) ∈ bag(C)

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``eclass0  class-ap``  0
  THEN  Unfold  `class-ap`  -3
  THEN  (RWO  "-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  ThinVars  [`X';`es';`e';`F'])\mcdot{})\mcdot{}

---

Home Index