---

Step * of Lemma local-class-output-agree

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[P:LocalClass(X)]. ∀[eo1,eo2:EO+(Info)]. ∀[e1:E]. ∀[e2:E].
  (X(e1) = X(e2) ∈ bag(A)) supposing (eo-local-agree(Info;eo1;eo2;e1;e2) and (loc(e1) = loc(e2) ∈ Id))
BY
{ (Auto
   THEN D 4
   THEN (InstHyp [⌈eo1⌉;⌈e1⌉] 5⋅ THENA Auto)
   THEN (InstHyp [⌈eo2⌉;⌈e2⌉] 5⋅ THENA Auto)
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN HypSubst' (-4) 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. 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)

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[P:LocalClass(X)].  \mforall{}[eo1,eo2:EO+(Info)].  \mforall{}[e1:E].  \mforall{}[e2:E].
    (X(e1)  =  X(e2))  supposing  (eo-local-agree(Info;eo1;eo2;e1;e2)  and  (loc(e1)  =  loc(e2)))


By

(Auto
  THEN  D  4
  THEN  (InstHyp  [\mkleeneopen{}eo1\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}eo2\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  HypSubst'  (-4)  0)

---

Home Index