---

Step * of Lemma eclass-events_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[L:E List].  (eclass-events(es;X;L) ∈ E(X) List)
BY
{ (Auto
   THEN (InstLemma `filter_type` [⌜E⌝;⌜λe.e ∈b X⌝;⌜L⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Fold `es-E-interface` (-1)
   THEN Fold `eclass-events` (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[L:E  List].    (eclass-events(es;X;L)  \mmember{}  E(X)  List)


By

---

Latex:
(Auto
  THEN  (InstLemma  `filter\_type`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}\mlambda{}e.e  \mmember{}\msubb{}  X\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `es-E-interface`  (-1)
  THEN  Fold  `eclass-events`  (-1)
  THEN  Auto)\mcdot{}

---

Home Index