---

Step * 1 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 : 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)
BY
{ (RWO "list-eo-info-before" 0 THENA (Try (BLemma `list-eo-E`) THEN 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*(firstn(||ms' @ [v]|| - 1;ms' @ [v]))(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  :  Id  {}\mrightarrow{}  hdataflow(Info;T)
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(P  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
7.  ms'  :  Info  List@i
8.  v  :  Info@i
\mvdash{}  (snd(P  loc*(map(\mlambda{}x.info(x);before(||ms'  @  [v]||  -  1)))(info(||ms'  @  [v]||  -  1))))
=  (snd(P  loc*(ms')(v)))


By

---

Latex:
(RWO  "list-eo-info-before"  0  THENA  (Try  (BLemma  `list-eo-E`)  THEN  Auto))

---

Home Index