---

Step * 1 of Lemma eclass0-bag-program_wf


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``eclass0-bag  class-ap``  0
  THEN  Unfold  `class-ap`  -5
  THEN  (RWO  "-5"  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'])

---

Home Index