---

Step * of Lemma bag-member-filter2

∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))
BY
{ (((UnivCD THENM D 0 THENM UnivCD) THENA (Try (InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2x.P[x]⌝]⋅) THEN Auto))
   THEN ((InstLemma `bag-member-filter-implies2` [⌜T⌝;⌜x⌝;⌜bs⌝;⌜P⌝]⋅ THEN Auto)
         THEN InstLemma `bag-member-filter-implies1` [⌜T⌝;⌜x⌝;⌜bs⌝;⌜P⌝]⋅
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].  \mforall{}[P:\{x:T|  x  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}].    uiff(x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]];x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x])\000C)


By

---

Latex:
(((UnivCD  THENM  D  0  THENM  UnivCD)
    THENA  (Try  (InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.P[x]\mkleeneclose{}]\mcdot{})  THEN  Auto)
    )
  THEN  ((InstLemma  `bag-member-filter-implies2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THEN  Auto)
              THEN  InstLemma  `bag-member-filter-implies1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{}
  )

---

Home Index