---

Step * of Lemma interface-predecessors-filter-image

∀[Info,A,B:Type]. ∀[f:A ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[e:E].
  (≤(f[X])(e) ~ filter(λe.(#(f X(e)) =z 1);≤(X)(e)))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``es-interface-predecessors eclass-events`` 0
   THEN RWO "filter-filter" 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN BLemma `filter-sq`
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (\mleq{}(f[X])(e)  \msim{}  filter(\mlambda{}e.(\#(f  X(e))  =\msubz{}  1);\mleq{}(X)(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-interface-predecessors  eclass-events``  0
  THEN  RWO  "filter-filter"  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  BLemma  `filter-sq`
  THEN  Reduce  0
  THEN  Auto)

---

Home Index