---

Step * 1 1 1 1 1 of Lemma base-process-class-program_wf


1. Info : Type
2. T : Type
3. loc : Id
4. X : EClass(T)
5. P : LocalClass(X)
6. ms' : Info List@i
7. v : Info@i
⊢ (X list-eo(ms' @ [v];loc) (||ms' @ [v]|| - 1)) = (snd(P loc*(ms')(v))) ∈ bag(T)
BY
{ (DVar `P'
   THEN Fold `class-ap` 0
   THEN (RWO "-3" 0 THENA (Try (BLemma `list-eo-E`) THEN Auto))
   THEN (RWO  "list-eo-loc" 0 THENA Auto)) }

1
1. Info : Type
2. T : Type
3. loc : Id
4. X : EClass(T)
5. P : Id ⟶ hdataflow(Info;T)
6. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(T))
7. ms' : Info List@i
8. v : Info@i
⊢ (snd(P loc*(map(λx.info(x);before(||ms' @ [v]|| - 1)))(info(||ms' @ [v]|| - 1)))) = (snd(P loc*(ms')(v))) ∈ bag(T)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  loc  :  Id
4.  X  :  EClass(T)
5.  P  :  LocalClass(X)
6.  ms'  :  Info  List@i
7.  v  :  Info@i
\mvdash{}  (X  list-eo(ms'  @  [v];loc)  (||ms'  @  [v]||  -  1))  =  (snd(P  loc*(ms')(v)))


By

---

Latex:
(DVar  `P'
  THEN  Fold  `class-ap`  0
  THEN  (RWO  "-3"  0  THENA  (Try  (BLemma  `list-eo-E`)  THEN  Auto))
  THEN  (RWO    "list-eo-loc"  0  THENA  Auto))

---

Home Index