---

Step * 1 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. (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)
BY
{ ((Reduce (-3) THEN FLemma `general-append-cancellation` [-3]) THEN Auto) }

---

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.  (map(\mlambda{}e.info(e);before(e1))  @  map(\mlambda{}e.info(e);[e1]))
=  (map(\mlambda{}e.info(e);before(e2))  @  map(\mlambda{}e.info(e);[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

((Reduce  (-3)  THEN  FLemma  `general-append-cancellation`  [-3])  THEN  Auto)

---

Home Index