---

Step * of Lemma es-interface-events-append

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[L1,L2:E List].
  (eclass-events(es;X;L1 @ L2) ~ eclass-events(es;X;L1) @ eclass-events(es;X;L2))
BY
{ ((UnivCD THENA Auto) THEN RW (AddrC [1] UnfoldTopAbC) 0) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. L1 : E List
5. L2 : E List
⊢ filter(λe.e ∈b X;L1 @ L2) ~ eclass-events(es;X;L1) @ eclass-events(es;X;L2)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[L1,L2:E  List].
    (eclass-events(es;X;L1  @  L2)  \msim{}  eclass-events(es;X;L1)  @  eclass-events(es;X;L2))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0)

---

Home Index