---

Step * of Lemma until-class-program_wf

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[Y:EClass(C)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
  (until-class-program(xpr;ypr) ∈ LocalClass((X until Y)))
BY
{ (Auto THEN D -2 THEN D -1 THEN Unfold `until-class-program` 0 THEN MemTypeCD THEN Auto) }

1
1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. Y : EClass(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. ypr : Id ⟶ hdataflow(Info;C)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(C))
10. es : EO+(Info)@i'
11. e : E@i
⊢ (X until Y)(e) = (snd((λi.hdf-until(xpr i;ypr i)) loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[Y:EClass(C)].  \mforall{}[xpr:LocalClass(X)].  \mforall{}[ypr:LocalClass(Y)].
    (until-class-program(xpr;ypr)  \mmember{}  LocalClass((X  until  Y)))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  Unfold  `until-class-program`  0  THEN  MemTypeCD  THEN  Auto)

---

Home Index