---

Step * 1 of Lemma eclass1-program_wf


1. Info : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. X : EClass(B)
6. f : Id ─→ B ─→ C
7. pr : Id ─→ hdataflow(Info;B)
8. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(pr 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.((f i) o (pr i))) loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(C)
BY
{ (RepUR ``eclass1 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';`pr'])⋅) }

1
1. Info : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. f : Id ─→ B ─→ C
6. es : EO+(Info)@i'
7. e : E@i
8. L : Info List@i
9. x : Info@i
10. h : hdataflow(Info;B)@i
⊢ bag-map(f loc(e);snd(h*(L)(x))) = (snd((f loc(e)) 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)
6.  f  :  Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C
7.  pr  :  Id  {}\mrightarrow{}  hdataflow(Info;B)
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(pr  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.((f  i)  o  (pr  i)))  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e))))


By

---

Latex:
(RepUR  ``eclass1  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';`pr'])\mcdot{})

---

Home Index