---

Step * 1 of Lemma local-class-output-agree


1. Info : Type
2. A : Type
3. X : EClass(A)
4. P : Id ─→ hdataflow(Info;A)
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. eo1 : EO+(Info)
7. eo2 : EO+(Info)
8. e1 : E
9. e2 : E
10. loc(e1) = loc(e2) ∈ Id
11. eo-local-agree(Info;eo1;eo2;e1;e2)
12. X(e1) = (snd(P loc(e1)*(map(λx.info(x);before(e1)))(info(e1)))) ∈ bag(A)
13. X(e2) = (snd(P loc(e2)*(map(λx.info(x);before(e2)))(info(e2)))) ∈ bag(A)
⊢ (snd(P loc(e2)*(map(λx.info(x);before(e1)))(info(e1))))
= (snd(P loc(e2)*(map(λx.info(x);before(e2)))(info(e2))))
∈ bag(A)
BY
{ (RepUR ``eo-local-agree es-le-before`` (-3)⋅ THEN (RWO "map_append_sq" (-3) THENA Auto) THEN Reduce 0) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. P : Id ─→ hdataflow(Info;A)
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. eo1 : EO+(Info)
7. eo2 : EO+(Info)
8. e1 : E
9. e2 : E
10. loc(e1) = loc(e2) ∈ Id
11. (map(λe.info(e);before(e1)) @ map(λe.info(e);[e1]))
= (map(λe.info(e);before(e2)) @ map(λe.info(e);[e2]))
∈ (Info List)
12. X(e1) = (snd(P loc(e1)*(map(λx.info(x);before(e1)))(info(e1)))) ∈ bag(A)
13. X(e2) = (snd(P loc(e2)*(map(λx.info(x);before(e2)))(info(e2)))) ∈ bag(A)
⊢ (snd(P loc(e2)*(map(λx.info(x);before(e1)))(info(e1))))
= (snd(P loc(e2)*(map(λx.info(x);before(e2)))(info(e2))))
∈ bag(A)

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  P  :  Id  {}\mrightarrow{}  hdataflow(Info;A)
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(P  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
6.  eo1  :  EO+(Info)
7.  eo2  :  EO+(Info)
8.  e1  :  E
9.  e2  :  E
10.  loc(e1)  =  loc(e2)
11.  eo-local-agree(Info;eo1;eo2;e1;e2)
12.  X(e1)  =  (snd(P  loc(e1)*(map(\mlambda{}x.info(x);before(e1)))(info(e1))))
13.  X(e2)  =  (snd(P  loc(e2)*(map(\mlambda{}x.info(x);before(e2)))(info(e2))))
\mvdash{}  (snd(P  loc(e2)*(map(\mlambda{}x.info(x);before(e1)))(info(e1))))
=  (snd(P  loc(e2)*(map(\mlambda{}x.info(x);before(e2)))(info(e2))))


By

(RepUR  ``eo-local-agree  es-le-before``  (-3)\mcdot{}
  THEN  (RWO  "map\_append\_sq"  (-3)  THENA  Auto)
  THEN  Reduce  0)

---

Home Index